search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

difference (check-sat a) vs. (check-sat-assuming (a)) #4549

Closed nicohaenggi closed 4 years ago

nicohaenggi commented 4 years ago

I recently worked my way through the Z3 SMT-LIB parser and realised that the following grammar is being parsed for the check-sat and check-sat-assuming commands:

<check_sat>           ::= (check-sat <term>*)
<check_sat_assuming>  ::= (check-sat-assuming (<term>*) )

Now from what I have found, there does not seem to be any documentation for the check-sat command supplied with (multiple) expression arguments. Since I'm assuming that these two commands are actually semantically equivalent, I have tested all check-sat-assuming commands from the Z3 test framework with check-sat. The Z3 solver returns the same result for both commands.

Is there any semantic difference between these two commands or am I missing something here?

NikolajBjorner commented 4 years ago

They are the same. The check-sat-assuming variant is described in the SMTLIB2 standard. Allowing check-sat to have multiple arguments was in z3 while formats were still in flux. It is available for convenience.

http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf