diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-10 19:10:06 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-10 19:10:06 -0500 |
| commit | 2f30f5dc342fa19b42842d744034f53a1dee3f43 (patch) | |
| tree | 10aa6d491a8d337bbbda3af456b96f0ed989bfb0 /test | |
| parent | 356647c4b7eb2420f6c6b350f0622bb4c863b0a5 (diff) | |
(proof-new) Remove arith-snorm option. (#4591)
This option only marginally helped and will be difficult to support with the new proof infrastructure.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress1/nl/issue3955-ee-double-notify.smt2 | 1 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ea1021d89..69378a559 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1502,7 +1502,6 @@ set(regress_1_tests regress1/quantifiers/anti-sk-simp.smt2 regress1/quantifiers/ari118-bv-2occ-x.smt2 regress1/quantifiers/arith-rec-fun.smt2 - regress1/quantifiers/arith-snorm.smt2 regress1/quantifiers/array-unsat-simp3.smt2 regress1/quantifiers/bi-artm-s.smt2 regress1/quantifiers/bignum_quant.smt2 @@ -2420,6 +2419,8 @@ set(regression_disabled_tests regress1/nl/NAVIGATION2.smt2 # sat or unknown in different builds regress1/nl/issue3307.smt2 + # no longer support snorm option + regress1/quantifiers/arith-snorm.smt2 # ajreynol: different error messages on production and debug: regress1/quantifiers/macro-subtype-param.smt2 # times out with competition build: diff --git a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 index 21f26df2d..a4d04a8f4 100644 --- a/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 +++ b/test/regress/regress1/nl/issue3955-ee-double-notify.smt2 @@ -1,7 +1,6 @@ ; COMMAND-LINE: --quiet
; EXPECT: sat
(set-logic QF_UFNRA)
-(set-option :snorm-infer-eq true)
(set-info :status sat)
(declare-const r0 Real)
(declare-const r4 Real)
|