Different verification results produced when there is only a variable name difference about uclid HOT 4 OPEN

Thanks for the report.

Can you explain to me why you think the expected result of "unknown" is correct? The ground truth is that the file is either SAT (fails verification) or UNSAT (passes verification), unknown is simply what the SMT solver reports when it can't figure out the actual answer.

I don't know why the SMT solver can find a solution in the second case but not in the first, I'll look into it, but note that if an "assert false" is unreachable, it will pass verification.

from uclid.

Thank you for the answer. Whenever assert false; statement could be reached in a path, uclid seems to generate an unknown (==UNDEF) result.

In the above examples, the point before call simple_test(); (line 1706) is always reachable. Thus, if simple_test() procedure is not malfunctioning, the point after call simple_test(); should be also reachable (line 1708), which is assert false;. I thought that [expected results] are generated, because assert false is reached as expected.

In contrast, while the same procedure is called and all the assumptions are the same, the assert false in line 1708 is not reached in the [unexpected results].

I am not sure why assert false is unreachable in the second case (unexpected results).

from uclid.

I think you have misunderstood the UNDEF/unknown results. All that means is that the SMT problem is too hard for the SMT solver to solve so we don't know whether your assert false is reachable or not. The correct result cannot ever be "undef" because the correct result is never "we don't know".

To summarise, for an assert false, if UCLID reports:

• verification failed (sat) - the assertion is definitely reachable
• verification passed (unsat) - the assertion is definitely unreachable
• undef (unknown) - the problem is too hard for the SMT solver. We don't know the answer.

We do not know if the line before simple_test is reachable either, because an assert false in that position is reported as UNDEF.

Take a look at the SMT files. The reason the files generated by your first branch are unknown is because there are a lot of difficult quantifiers. This is a much simplified version of part of one of your queries and an SMT solver reports unknown:

(set-logic ALL)
(declare-fun f (Int) Int)
(assert (forall ((v1 Int) (v2 Int))
  (or (not (= (f v1)(f v2)))
         (= v1 v2))
))
(check-sat)

The reason the second file can be verified, is the final two assertions are trivial to solve:

(assert (not (and (= havoc_172_proof_op tap_proof_op_enter) (not havoc_95_done))))
(assert (and (= havoc_172_proof_op tap_proof_op_enter) (not havoc_95_done)))

Without going into your proofs in detail, I'm not sure where these conflicting assertions have come from. I am happy to take a look if you can provide a more minimal input

from uclid.

Thank you for the detailed answer. I seem to have misunderstood the UNDEF/unknown results.

I've made another example, but removed it because there was a logic error in that example.

from uclid.