Different Results from API and Binary

[avery-laird]

Hello,

I'm experiencing some cases where results from the C++ API and the binary seem to differ. One example of my issue is the following:

• Issue commands from the C++ API, using a solver with set("smtlib2_log", "<log-file>.smt2")
  • get results like sat, sat
• run z3 <log-file>.smt2
  • get results like sat, unsat

The binary and API are the same versions (built from the same repo). After every (check-sat) is a (reset) command. No incremental commands are used. I cannot publish example queries publicly but could provide logs privately if possible.

Are there any common reasons why this behaviour could occur? I assume I may be making some simple mistake, but I've tried everything I can think of. Any suggestions or help is greatly appreciated.

[NikolajBjorner]

Not sure. smtlib2_log is only used on occasion so may have its own bugs that have been undetected.
you can try to send me material and I will look into it.

[avery-laird]

Great, thank you. I will send more detail to nbjorner@microsoft.com

[avery-laird]

After an email exchange: @NikolajBjorner identifies this as an unsoundness bug, so I will leave this issue open for now.

[NikolajBjorner]

this got fixed, but it also establishes that the second query can't be solved (z3 loops).
The issue with the second query was a quantifier under the scope of a recursively defined function.
This wasn't even supported until recently, but the support came with a bug: it would jump to base level 0 when compiling a quantified function case into formulas. However, for recursive functions z3 relies on iterative deepening based on assumptions. The scope level of assumptions is 1. It should never have backtracked below level 1.