diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-05 13:32:35 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-05 13:32:35 -0500 |
| commit | c03e334d8d204d4083c4bdf2674d1438fdeab394 (patch) | |
| tree | 41b31d81af422e7143875ac63745375b7df77940 /test | |
| parent | d14cb15be7eb3482afeec277d56d6ed2e9cdc76a (diff) | |
Fix bug 698.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/nl/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/nl/bug698.smt2 | 5 |
2 files changed, 7 insertions, 1 deletions
diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index a422c9045..13f561130 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -45,7 +45,8 @@ TESTS = \ nl-help-unsat-quant.smt2 \ metitarski-3-4.smt2 \ rewriting-sums.smt2 \ - disj-eval.smt2 + disj-eval.smt2 \ + bug698.smt2 # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/nl/bug698.smt2 b/test/regress/regress0/nl/bug698.smt2 index 4f0d6102b..ba7610145 100644 --- a/test/regress/regress0/nl/bug698.smt2 +++ b/test/regress/regress0/nl/bug698.smt2 @@ -1,6 +1,8 @@ +; COMMAND-LINE: --incremental --nl-alg --fmf-fun-rlv --no-check-models (set-logic UFNIA) (set-info :smt-lib-version 2.5) +; EXPECT: sat (declare-fun fixedAdd() Int) (assert (= fixedAdd (+ 2 (+ 2 (+ 2 0))))) (check-sat) @@ -10,14 +12,17 @@ 0 (+ a ($$add$$ a (- b 1))))) +; EXPECT: sat (declare-fun variableAdd() Int) (assert (= variableAdd ($$add$$ 2 3))) (check-sat) +; EXPECT: sat (declare-fun fixedTimes() Int) (assert (= fixedTimes (* 2 (* 2 (* 2 1))))) (check-sat) +; EXPECT: sat (define-fun-rec $$pow$$ ((a Int)(b Int)) Int (ite (= b 0) 1 |