1

In the following code, I put a clearly unsatisfiable Z3 declaration and then try to use the C++/C Z3 APIs to see it programmatically solved.

The problem is that this code always triggers the check that outputs: "SAT?!". i.e. the clearly unsatisfiable expression is determined to be satisfiable in the current usage of the API calls.

How can I get this kind of operation to work as expected?

#include "z3++.h"
int main(){
  z3::context c;

  std::string testing = "(declare-const p0 Bool)(assert(= p0 true))(assert(= p0 false))(check-sat)";

  Z3_ast parsed = Z3_parse_smtlib2_string(c,testing.c_str(),0,0,0,0,0,0);
  z3::expr e(c, parsed);

  z3::solver s(c);
  if(s.check() == z3::sat)
    std::cout << "SAT?!\n";
  return 0;
}
d'alar'cop
  • 2,357
  • 1
  • 14
  • 18

1 Answers1

2

Z3 is correct in this case, because no constraints have been added to the solver, thus this is trivially satisfiable. The crucial part is this:

Z3_ast parsed = Z3_parse_...
z3::expr e(c, parsed);

z3::solver s(c);
s.add(e); // <--- Add constraints to solver here
if(s.check() ...
Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • It worked! Thank you. note to that MS researcher of SO: maybe you can see that there needs to be some improvement to the documentation and examples for this very good theorem prover. – d'alar'cop Jul 02 '14 at 11:56
  • For the C++ API there is an example that shows most of the basic concepts here: https://z3.codeplex.com/SourceControl/latest#examples/c++/example.cpp The API documentations are here: http://research.microsoft.com/en-us/um/redmond/projects/z3/index.html – Christoph Wintersteiger Jul 02 '14 at 12:31
  • I saw these, but there are many things that one would normally wish to do which one is left to (as a Z3 amateur) hunt around for painstakingly. Those brilliant enough to give birth to such a product should find it quite possible to make using it much easier. – d'alar'cop Jul 02 '14 at 12:47
  • There is another Z3 question here: http://stackoverflow.com/questions/24566727/implement-z3-maximize-in-c – d'alar'cop Jul 04 '14 at 04:31