diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/repair-const-nterm.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/repair-const-nterm.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
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) |