From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 21 Aug 2018 21:14:55 +0000 (-0500)
Subject: Makes the new row propagation system default (#2335)
X-Git-Tag: cvc5-1.0.0~4747
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a1b769fcb9ecdab7c09d7d7f05e4f87f54133076;p=cvc5.git

Makes the new row propagation system default (#2335)
---

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 7bfe8d592..80403ee0d 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -225,7 +225,7 @@ header = "options/arith_options.h"
   category   = "regular"
   long       = "new-prop"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "use the new row propagation system"
 
 [[option]]
diff --git a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
index d7a082304..47006622d 100644
--- a/test/regress/regress0/nl/ext-rew-aggr-test.smt2
+++ b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg --no-new-prop
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_NIA)
diff --git a/test/regress/regress1/nl/metitarski-1025.smt2 b/test/regress/regress1/nl/metitarski-1025.smt2
index 5a95364f3..73a132350 100644
--- a/test/regress/regress1/nl/metitarski-1025.smt2
+++ b/test/regress/regress1/nl/metitarski-1025.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext --no-new-prop
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |
diff --git a/test/regress/regress1/nl/metitarski-3-4.smt2 b/test/regress/regress1/nl/metitarski-3-4.smt2
index 835d60732..3a1e794cc 100644
--- a/test/regress/regress1/nl/metitarski-3-4.smt2
+++ b/test/regress/regress1/nl/metitarski-3-4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext
+; COMMAND-LINE: --nl-ext --no-new-prop
 ; EXPECT: sat
 (set-logic QF_NRA)
 (set-info :source |