From a98cd6d50308d1dde1086f0c1502e022bd30ba1b Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 21 Feb 2020 16:16:19 -0800 Subject: Switch to th_lira.plf (#3741) Switches arith_proof.cpp from th_lra to th_lira. Changes: Eliminate the d_realMode hack. instead: modify printOwnedTermAsType prints as integers OR reals, depending on expectedType. simultaneously: write printOwnedTermAsType more concisely also: reimplement printOwnedSort. Change to the LIRA axioms: Because they reason about bound types using side conditions, we no longer need to worry about choosing the correct strictness for our axiom. This allows us to cut out a lot of code, rewriting & shrinking printTheoryLemmaProof. They also have different names. This requires us to change a lot of string literals enable proof-checking for many tests. --- test/regress/regress0/arith/integers/ackermann5.smt2 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test/regress/regress0/arith/integers/ackermann5.smt2') diff --git a/test/regress/regress0/arith/integers/ackermann5.smt2 b/test/regress/regress0/arith/integers/ackermann5.smt2 index 8b93a3c35..debd29344 100644 --- a/test/regress/regress0/arith/integers/ackermann5.smt2 +++ b/test/regress/regress0/arith/integers/ackermann5.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores +; COMMAND-LINE: --ackermann --no-check-models ; EXPECT: sat (set-logic QF_UFLIA) (set-info :smt-lib-version 2.0) -- cgit v1.2.3