# Simple Min/Max case

 DinSoft Mar 21, 2010 at 3:03 AM Hi all, I'm trying to play a little bit with VCC (right now I stick to very basic cases). It was successfully able to verify the following program: ```#define MIN(a, b) (((a) < (b)) ? (a) : (b)) #define MAX(a, b) (((a) > (b)) ? (a) : (b)) unsigned int midvalue(unsigned int a, unsigned int b, unsigned int c) requires(a != b && a != c && b != c) ensures(MIN(MIN(a, b), c) < result < MAX(MAX(a, b), c)) { return MIN(MIN(MAX(a, b), MAX(b, c)), MAX(a, c)); } ``` However, for some reason, if I drop the "unsigned" restriction, it does not verify anymore. Any idea why ? I did not extensively test this basic case but it seems correct to me, even without the "unsigned". Many thanks, Regards,  Dinesh Bolkensteyn fdupress Editor Mar 21, 2010 at 8:17 AM Hi Dinesh, Like all sound verifiers, VCC is incomplete: some valid programs will fail to verify. In your case, the formula you are asking it to prove: `MIN(MIN(a, b), c) < MIN(MIN(MAX(a, b), MAX(b, c)), MAX(a, c)) < MAX(MAX(a, b), c)` is a bit too complex. In the case of unsigned integers, it can make the simplifying assumption that a, b and c are positive. When you work with signed integers, the full complexity of the formula appears, and VCC (or Z3) simply can't handle it. Although I can't give you an in-depth explanation of why the proof fails, i can give you a simple way of making it go through: if you break your formula into two simpler formulas, the verification succeeds again, even in the signed case.   int midvalue(int a, int b, int c) requires(a != b && a != c && b != c) ensures(MIN(MIN(a, b), c) < result && result < MAX(MAX(a, b), c)) { return MIN(MIN(MAX(a, b), MAX(b, c)), MAX(a, c)); }     ```#define MIN(a, b) (((a) < (b)) ? (a) : (b)) #define MAX(a, b) (((a) > (b)) ? (a) : (b)) int midvalue(int a, int b, int c) requires(a != b && a != c && b != c) ensures(MIN(MIN(a, b), c) < result && result < MAX(MAX(a, b), c)) { return MIN(MIN(MAX(a, b), MAX(b, c)), MAX(a, c)); } ``` In general, if something you believe is true fails to verify, try to simplify the manipulated formulas; it usually helps a lot. Cheers, Francois stobies Coordinator Mar 24, 2010 at 1:19 PM Edited Mar 24, 2010 at 1:23 PM Hi Dinesh, Francois, in C, 'a < b -2147483022:int b -> -3774:int c -> -2147483023:int   If you fix your example and write MIN(MIN(a, b), c) < result && result < MAX(MAX(a, b), c)), as Francois suggested, then VCC verifies your code. Not because the code is now simpler, but because the code is now correct. MarkHillebrand Coordinator Mar 25, 2010 at 10:05 AM Let me add that with increased warning level (giving /w:2 as a command-line option), VCC produces a warning for the original code hinting at the potential problem: d:\viridian_mah\vmhv\dinsoft.c(8,12) : warning VC9003: '((((((a) < (b)) ? (a) : (b))) < (c)) ? ((((a) < (b)) ? (a) : (b))) : (c)) < result < ((((((a) > (b)) ? ( a) : (b))) > (c)) ? ((((a) > (b)) ? (a) : (b))) : (c))' probably does not expres s what you intended; use two conjoined conditions to express an interval or pare nthesize the left comparison. warning VC9003: '((((((a) < (b)) ? (a) : (b))) < (c)) ? ((((a) < (b)) ? (a) : (b))) : (c)) < result < ((((((a) > (b)) ? (a) : (b))) > (c)) ? ((((a) > (b)) ? (a) : (b))) : (c))' probably does not express what you intended; use two conjoined conditions to express an interval or parenthesize the left comparison. Best, Mark