I am looking at verifying machine code programs. Since lots of modern SMT solver efficiently support arrays, I was planning to use them in our verification tool. I was playing around with z3 and I noticed that a small change to a formula results in timeout.
Here are the two examples that I used:
1) http://rise4fun.com/Z3/e4Ci *Formula: = (array_32_8_0_1_0 == array_32_8_0_0_0) And (EBP_1_1_0 == EBP_1_0_0) And (Not(array_32_8_0_1_0[EBP_1_1_0 - 0] == array_32_8_0_1_0[EBP_1_0_0 - 0]))* For this example, I get unsat, which is good!
2) http://rise4fun.com/Z3/t8aT *Formula: = (array_32_8_0_1_0 == array_32_8_0_0_0) And (EBP_1_1_0 == EBP_1_0_0) And (Not(array_32_8_0_1_0[EBP_1_1_0 - 1] == array_32_8_0_1_0[EBP_1_0_0 - 1]))* For this example, I get a timeout. On my machine running it with z3.exe for an hour didn't give me anything as well. This example is pretty much the same as (1) except the array access involves a linear expression. (Look at the definition of temp-var-4 at line 16)
Why is this happening? Does it have to do with combination of bit-vector and array theories?