diff options
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 |