diff options
Diffstat (limited to 'test/regress')
| -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)
|