diff options
Diffstat (limited to 'test/regress/regress4/siegel-nl-bases.smt2')
| -rw-r--r-- | test/regress/regress4/siegel-nl-bases.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress4/siegel-nl-bases.smt2 b/test/regress/regress4/siegel-nl-bases.smt2 new file mode 100644 index 000000000..cf6e3ab5e --- /dev/null +++ b/test/regress/regress4/siegel-nl-bases.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NIA) +(declare-const n Int) +(declare-const i1 Int) +(declare-const i2 Int) +(declare-const j1 Int) +(declare-const j2 Int) +(assert (>= n 0)) +(assert (not (= i1 i2))) +(assert (<= 0 i1)) +(assert (<= i1 j1)) +(assert (< j1 n)) +(assert (<= 0 i2)) +(assert (<= i2 j2)) +(assert (< j2 n)) +(assert (or + (= (+ (* i1 n) j1) (+ (* i2 n) j2)) + (= (+ (* i1 n) j1) (+ (* j2 n) i2)) + (= (+ (* j1 n) i1) (+ (* i2 n) j2)) + (= (+ (* j1 n) i1) (+ (* j2 n) i2)))) +(check-sat) |