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/regress1/nl | |
| 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/regress1/nl')
| -rw-r--r-- | test/regress/regress1/nl/iand-native-1.smt2 | 19 | ||||
| -rw-r--r-- | test/regress/regress1/nl/ufnia-factor-open-proof.smt2 | 14 |
2 files changed, 0 insertions, 33 deletions
diff --git a/test/regress/regress1/nl/iand-native-1.smt2 b/test/regress/regress1/nl/iand-native-1.smt2 deleted file mode 100644 index 0835b7066..000000000 --- a/test/regress/regress1/nl/iand-native-1.smt2 +++ /dev/null @@ -1,19 +0,0 @@ -; COMMAND-LINE: --iand-mode=value -; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find -; COMMAND-LINE: --iand-mode=bitwise -; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=1 -; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=2 -; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=4 -; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=5 -; COMMAND-LINE: --iand-mode=bitwise --bvand-integer-granularity=6 -; EXPECT: sat -(set-logic QF_NIA) -(set-info :status sat) -(declare-fun x () Int) -(declare-fun y () Int) - -(assert (and (<= 0 x) (< x 16))) -(assert (and (<= 0 y) (< y 16))) -(assert (> ((_ iand 4) x y) 0)) - -(check-sat) diff --git a/test/regress/regress1/nl/ufnia-factor-open-proof.smt2 b/test/regress/regress1/nl/ufnia-factor-open-proof.smt2 deleted file mode 100644 index bcb077f4f..000000000 --- a/test/regress/regress1/nl/ufnia-factor-open-proof.smt2 +++ /dev/null @@ -1,14 +0,0 @@ -(set-logic QF_UFNIA) -(set-info :status unsat) -(declare-fun pow2 (Int) Int) -(define-fun intmax ((k Int)) Int (- (pow2 k) 1)) -(define-fun intmodtotal ((pow2 Int) (a Int) (b Int)) Int (mod a b)) -(define-fun intneg ((k Int) (a Int)) Int 1) -(define-fun intmul ((k Int) (a Int) (b Int)) Int (mod (* a b) (pow2 k))) -(declare-fun k () Int) -(assert (> k 0)) -(assert (= 1 (pow2 1))) -(declare-fun %x () Int) -(assert (> %x 0)) -(assert (not (= (intmul k %x (intmax k)) (mod (- (pow2 k) %x) (pow2 k))))) -(check-sat) |