diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-19 15:06:41 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-19 15:06:41 -0600 |
| commit | 6d6428a609d76e62cec5ff0ce2bad36e8afe2601 (patch) | |
| tree | 226eebaf543931695261df46d32cc36b98396bf7 /test/regress | |
| parent | 0d949be444e52f42de4f920d71512c95ff96666d (diff) | |
Use new let binding utility in smt2 printer (#5472)
Also fixes some whitespace issues in printing quantified formulas.
Diffstat (limited to 'test/regress')
4 files changed, 10 insertions, 10 deletions
diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2 index 017479871..14f2316a7 100644 --- a/test/regress/regress0/printer/let_shadowing.smt2 +++ b/test/regress/regress0/printer/let_shadowing.smt2 @@ -2,8 +2,8 @@ ; COMMAND-LINE: --dump raw-benchmark --preprocess-only ; SCRUBBER: grep assert ; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0)))) -; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0) ))))) -; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))) ) ))))) +; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0)))))) +; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))))))))) (set-logic NIA) (declare-const _let_0 Int) (declare-const x Int) diff --git a/test/regress/regress1/quantifiers/dump-inst-i.smt2 b/test/regress/regress1/quantifiers/dump-inst-i.smt2 index 8a9f10ea7..fab0e3f0c 100644 --- a/test/regress/regress1/quantifiers/dump-inst-i.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst-i.smt2 @@ -1,17 +1,17 @@ ; COMMAND-LINE: --dump-instantiations --incremental --print-inst-full ; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/' ; EXPECT: unsat -; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x))) ; EXPECT: ( skv_TERM ) ; EXPECT: ) -; EXPECT: (instantiations (forall ((x Int)) (P x) ) +; EXPECT: (instantiations (forall ((x Int)) (P x)) ; EXPECT: ( skv_TERM ) ; EXPECT: ) ; EXPECT: unsat -; EXPECT: (skolem (forall ((x Int)) (or (P x) (R x)) ) +; EXPECT: (skolem (forall ((x Int)) (or (P x) (R x))) ; EXPECT: ( skv_TERM ) ; EXPECT: ) -; EXPECT: (instantiations (forall ((x Int)) (P x) ) +; EXPECT: (instantiations (forall ((x Int)) (P x)) ; EXPECT: ( skv_TERM ) ; EXPECT: ) (set-logic UFLIA) diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 index f900e78a9..274fc213f 100644 --- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2 @@ -1,10 +1,10 @@ ; REQUIRES: proof ; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full ; EXPECT: unsat -; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x))) ; EXPECT: ( 2 ) ; EXPECT: ) -; EXPECT: (instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))) ) +; EXPECT: (instantiations (forall ((x Int)) (or (not (S x)) (not (Q x)))) ; EXPECT: ( 2 ) ; EXPECT: ) (set-logic UFLIA) diff --git a/test/regress/regress1/quantifiers/dump-inst.smt2 b/test/regress/regress1/quantifiers/dump-inst.smt2 index d15025900..6ded98602 100644 --- a/test/regress/regress1/quantifiers/dump-inst.smt2 +++ b/test/regress/regress1/quantifiers/dump-inst.smt2 @@ -1,10 +1,10 @@ ; COMMAND-LINE: --dump-instantiations --print-inst-full ; SCRUBBER: sed -e 's/skv_.* )$/skv_TERM )/' ; EXPECT: unsat -; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x)) ) +; EXPECT: (skolem (forall ((x Int)) (or (P x) (Q x))) ; EXPECT: ( skv_TERM ) ; EXPECT: ) -; EXPECT: (instantiations (forall ((x Int)) (P x) ) +; EXPECT: (instantiations (forall ((x Int)) (P x)) ; EXPECT: ( skv_TERM ) ; EXPECT: ) (set-logic UFLIA) |