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/regress2 | |
| parent | 0073464e433e80311269ce07e0fa5de417b5eefc (diff) | |
Move slow nl regression to regress3 (#4276)
Should fix nightlies.
Diffstat (limited to 'test/regress/regress2')
| -rw-r--r-- | test/regress/regress2/nl/siegel-nl-bases.smt2 | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/test/regress/regress2/nl/siegel-nl-bases.smt2 b/test/regress/regress2/nl/siegel-nl-bases.smt2 deleted file mode 100644 index cf6e3ab5e..000000000 --- a/test/regress/regress2/nl/siegel-nl-bases.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -; 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) |