diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-05-07 16:30:48 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-07 23:30:48 +0000 |
| commit | 080f0de4379c4e1fe5a016e40c7852a3abb52760 (patch) | |
| tree | bdb25341973ace0bed5d4acfb3517e8cb6dd59fc /test/regress/regress4 | |
| parent | 5bd2fcd60adbfb1f1941d4ed9da6ec10e06dfb12 (diff) | |
Move slow regressions and update guidelines. (#6508)
This moves regression test that exceed the time limit of their
respective level to the appropriate level. It further updates the
guidelines in the README with information on how to properly categorize
regression tests into levels (with time limits).
Note: Test regress3/issue4717.smt2 was previously unsolved (unknown) and
is now sat (Z3 agrees).
Diffstat (limited to 'test/regress/regress4')
| -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) |