diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-12 11:01:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-12 11:01:24 -0500 |
commit | 9cd5bbf8c659d2e260bad71a841f5153f358a58b (patch) | |
tree | 2d160602ad2280bb32b1bb6a856d23c4f76fd92d /test/regress/regress3 | |
parent | 0073464e433e80311269ce07e0fa5de417b5eefc (diff) |
Move slow nl regression to regress3 (#4276)
Should fix nightlies.
Diffstat (limited to 'test/regress/regress3')
-rw-r--r-- | test/regress/regress3/siegel-nl-bases.smt2 | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress3/siegel-nl-bases.smt2 b/test/regress/regress3/siegel-nl-bases.smt2 new file mode 100644 index 000000000..cf6e3ab5e --- /dev/null +++ b/test/regress/regress3/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) |