Returning unknown not sat/unsat with jsmtlib

StackOverflow https://stackoverflow.com/questions/12535568

  •  03-07-2021
  •  | 
  •  

Question

Following this tutorial, I tried this first example in the tutorial.

(set-option :print-success false)
(set-logic QF_UF)
(declare-fun p () Bool)
(assert (and p (not p)))
(check-sat)
(exit)

I executed this command 

java -jar jsmtlib.jar test1.smt

To get unknown not unsat as in the tutorial.

What might be wrong with this?

Was it helpful?

Solution

I needed to specify what solver do I use. I chose yices as the server, and with java -jar jsmtlib.jar --solver yices --exec ./yices test1.smt, everything works fine.

OTHER TIPS

I believe jsmtlib.jar is some kind of wrapper for SMT solvers. The "unknown" answer has nothing to do with Z3. You should contact jsmtlib.jar authors about this problem.

Have you tried to use Z3 directly? It returns unsat for this script. You can try Z3 online at: http://rise4fun.com/Z3/chyM

We also have online tutorials: http://rise4fun.com/Z3/tutorial/guide

You can also download and install Z3 in your machine: http://research.microsoft.com/en-us/um/redmond/projects/z3/download.html

Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top