veriT solver says "unknown logic AUFNIRA"

[johnyf]

Using tlapm version 1.4.3 (adjusted to call veriT instead of verit https://github.com/johnyf/tlaps/tree/d6105dc6b31fe76acdeb83ef3ffcefa3ab8e04a5, see #18), with the input:

---- MODULE Foo ----
EXTENDS TLAPS

THEOREM TRUE
BY veriT
======================

and running veriT , I get the error:

launching process: "file=Foo.tlaps/tlapm_a57529.smt2; PATH="${PATH}:some/path/bin:some/path/lib/tlaps/bin"; veriT --input=smtlib2 --disable-ackermann --disable-banner --disable-print-success "$file" >Foo.tlaps/tlapm_a57529.smt2.out"
(* ... trivial *)
(error "unknown logic AUFNIRA")
(* created new "Foo.tlaps/Foo.thy" *)
(* fingerprints written in "Foo.tlaps/fingerprints" *)
File "./Foo.tla", line 21, characters 5-6:
Error: Could not prove or check:
         ASSUME veriT 
         PROVE  TRUE
File "./Foo.tla", line 1, character 1 to line 55, character 80:
Error: 1/2 obligation(s) failed
FATAL: there were backend errors processing module "Foo"
 tlapm ending abnormally with Failure("backend errors")

I tried the following veriT versions:

• stable2016
• smtcomp2014
• 201410
• 201310

I wasn't able to find a download for "veriT-nla-201311 (veriT + REDUCE with support for non-linear arithmetics)" (mentioned in the older veriT website). Not sure whether that version supports the logic AUFNIRA.

The SMT file given as input to veriT contained:

;; Proof obligation:
;;TRUE
(set-logic AUFNIRA)
(declare-sort u 0)
;; Declaration of terms, predicates and strings
;; Axioms
;; Conclusion
(assert (not true))
;; Main assertions from the proof obligation
(check-sat)

Sidenote: In order to capture the SMT file that tlapm generates for the solver, I invoked tlapm with

tlapm --solver "cp \"\$file\" ../" -v --cleanfp Foo.tla

In order to get cp to run, the input should be changed to:

---- MODULE Foo ----
EXTENDS TLAPS

THEOREM TRUE
BY OBVIOUS
======================