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

tptp4x error when translating `$false` or `$true` to SMT-LIB 2 #79

Closed asr closed 7 years ago

asr commented 7 years ago 
$ cat bug.fof
fof(foo, conjecture, $true | $false).

Using tptp4X for translating the above file to smt2 we get

$ tptp4X -fsmt2 bug.fof > bug.smt2
$ cat bug.smt2
(set-logic UF)
(declare-sort sort__smt2 0)
; functions
; predicates
(declare-fun true__smt2_0 ( ) Bool)
(declare-fun false__smt2_0 ( ) Bool)

;----This is the conjecture with negated conjecture
; foo conjecture
(assert (not (or true__smt2_0
        false__smt2_0)))

(check-sat)

Note that $false and $true are incorrectly translated to false__smt2_0 and true__smt2_0, respectively. The correct translation is false and true. In consequence, Z3 fails for proving theorems including $false or $true.