search

asr / apia

Haskell program for proving first-order theorems written in Agda using automatic theorem provers for first-order logic
MIT License
6 stars 0 forks source link

Z3 exit status #64

Closed asr closed 7 years ago

asr commented 8 years ago

Apia search the string "unsat" in the output of Z3 for determining if Z3 proved a conjecture.

The following example shows that even when Z3 found an error, it generates the string "unsat":

$ cat test.smt2
(set-logic QF_UF)
(declare-fun A () Bool)
(declare-fun B⇒ () Bool)
(assert (not (=> A A)))
(check-sat)
$ z3 test.smt2 
(error "line 3 column 14: unexpected character")
(error "line 3 column 15: unexpected character")
(error "line 3 column 16: unexpected character")
unsat
$ echo $?
1
$ z3 --version
Z3 version 4.5.0 - 64 bit

That is, in addition to search the string "unsat" it is necessary to check the exit status of Z3.

asr commented 7 years ago

Partially blocked by https://github.com/Z3Prover/z3/issues/859.