diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-05 17:41:18 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-05 17:41:18 -0500 |
| commit | f4b158635255affcafe52c7664fc5de4660c3f83 (patch) | |
| tree | c22a6b39b7b8137b5ca476188b4d8fad1430f45c /test | |
| parent | 5ce46e8a6ac10388b7a2032c7d67a81da0edbd5e (diff) | |
Do not eliminate extended arithmetic symbols when finite model finding is on, add regression.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 | 25 |
2 files changed, 27 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 593cdfa8b..b02443989 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -73,7 +73,8 @@ TESTS = \ constr-ground-to.smt2 \ bug-041417-set-options.cvc \ alg202+1.smt2 \ - fmf-fun-no-elim-ext-arith.smt2 + fmf-fun-no-elim-ext-arith.smt2 \ + fmf-fun-no-elim-ext-arith2.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 new file mode 100644 index 000000000..ea5a5e4b7 --- /dev/null +++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2 @@ -0,0 +1,25 @@ +; COMMAND-LINE: --fmf-fun --no-check-models +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool ( + or + (= n1 n 0) + (= n2 n 0) + ( + and + (> n1 0) + (> n2 0) + (>= n 0) + (= (not (= (mod n 2 ) 0)) (and (not (= (mod n1 2 ) 0)) (not (= (mod n2 2) 0)))) + (int-and (div n 2) (div n1 2) (div n2 2)) + ) +)) +(declare-const x Int) +(declare-const y Int) +(declare-const z Int) +(assert (= x 1)) +(assert (= y 1)) +(assert (= z 1)) +(assert (int-and z x y)) +(check-sat) |