diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 | 15 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/repair-const-nterm.smt2 | 12 |
3 files changed, 29 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 0b9e415fa..017e4f9bd 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1251,6 +1251,7 @@ REG1_TESTS = \ regress1/quantifiers/NUM878.smt2 \ regress1/quantifiers/RND-small.smt2 \ regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 \ + regress1/quantifiers/RND_4_1-existing-inst.smt2 \ regress1/quantifiers/RND_4_16.smt2 \ regress1/quantifiers/anti-sk-simp.smt2 \ regress1/quantifiers/ari118-bv-2occ-x.smt2 \ @@ -1308,6 +1309,7 @@ REG1_TESTS = \ regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \ regress1/quantifiers/qcft-smtlib3dbc51.smt2 \ regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \ + regress1/quantifiers/repair-const-nterm.smt2 \ regress1/quantifiers/recfact.cvc \ regress1/quantifiers/rew-to-0211-dd.smt2 \ regress1/quantifiers/ricart-agrawala6.smt2 \ diff --git a/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 b/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 new file mode 100644 index 000000000..73c278522 --- /dev/null +++ b/test/regress/regress1/quantifiers/RND_4_1-existing-inst.smt2 @@ -0,0 +1,15 @@ +(set-logic LRA) +(set-info :status unsat) +(declare-fun a () Real) +(assert + (forall ((?y2 Real) (?y3 Real)) + (or + (= ?y3 1) + (> ?y3 0) + (and + (< ?y2 0) + (< ?y3 49) + ))) +) +(check-sat) +(exit) diff --git a/test/regress/regress1/quantifiers/repair-const-nterm.smt2 b/test/regress/regress1/quantifiers/repair-const-nterm.smt2 new file mode 100644 index 000000000..f9b1d6829 --- /dev/null +++ b/test/regress/regress1/quantifiers/repair-const-nterm.smt2 @@ -0,0 +1,12 @@ +(set-logic LIA) +(set-info :status unsat) + +(declare-fun k_20 () Int) +(declare-fun k_72 () Int) +(declare-fun k_73 () Int) + +(assert +(forall ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) (not (>= (+ (* 3 x7) (* (- 1) (ite (= x7 k_20) k_72 k_73))) 1)) ) +) + +(check-sat) |