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 doesn't prove a theorem #25

Closed asr closed 7 years ago

asr commented 8 years ago

From @asr on October 5, 2015 20:41

$ z3 --version
Z3 version 4.4.1
$ cd test/succeed/fol-theorems
$ agda Definition10.agda
$ apia --atp=z3 --time=10 Definition10.agda
...
Proving the conjecture in /tmp/Definition10/48-A0.fof
/tmp/Definition10/48-A0.fof -> /tmp/Definition10///48-A0.smt2
Z3 version 4.4.1 *did not* prove the conjecture

I reported the issue (see https://github.com/Z3Prover/z3/issues/231).