Fix for logic info, update regressions. Update casc tfa script.

diff --git a/contrib/run-script-casc26-tfa b/contrib/run-script-casc26-tfa
index 05062bf5cf3ec5eaa7f1040fbf7ac4ad9b4c7e57..74147e5298c0fd585b4d4434ceb2310bbbeff520 100644 (file)
--- a/contrib/run-script-casc26-tfa
+++ b/contrib/run-script-casc26-tfa
@@ -29,11 +29,9 @@ function finishwith {
   $cvc4 --lang=tptp --no-checking --no-interactive --force-logic="UFNIRA" --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench
 }
 
-trywith 10 --decision=internal --full-saturate-quant
-trywith 10 --finite-model-find --decision=internal
-trywith 10 --multi-trigger-when-single --multi-trigger-priority --nl-ext --nl-ext-tplanes --full-saturate-quant
-trywith 10 --partial-triggers --full-saturate-quant
+trywith 15 --finite-model-find --decision=internal
+trywith 15 --multi-trigger-when-single --multi-trigger-priority --nl-ext-tplanes --full-saturate-quant
+trywith 15 --no-e-matching --full-saturate-quant 
 trywith 15 --cbqi-all --purify-triggers --full-saturate-quant 
-trywith 15 --nl-ext --fs-inst --full-saturate-quant
-finishwith --macros-quant --macros-quant-mode=all --full-saturate-quant
+finishwith --macros-quant --macros-quant-mode=all --nl-ext-tplanes --full-saturate-quant
 # echo "% SZS status" "GaveUp for $filename"

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 6f519c15fe5772e006e3659ef787ab98417ff524..3a89ca0486ffceb48f161ff830809e2a29354685 100644 (file)
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -36,7 +36,7 @@ LogicInfo::LogicInfo() :
   d_sharingTheories(0),
   d_integers(true),
   d_reals(true),
-  d_linear(true),// for now, "everything enabled" doesn't include non-linear arith
+  d_linear(false),
   d_differenceLogic(false),
   d_cardinalityConstraints(false),
   d_locked(false) {

diff --git a/test/regress/regress0/expect/scrub.06.cvc b/test/regress/regress0/expect/scrub.06.cvc
index 8961493348a0f8e0274b14092a265c745176c1fe..2656c71b3b51ef09266f96ea7140aa794ba0dd54 100644 (file)
--- a/test/regress/regress0/expect/scrub.06.cvc
+++ b/test/regress/regress0/expect/scrub.06.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --force-logic=QF_LRA
 % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' -e '/^$/d'
 % EXPECT: A non-linear fact was asserted to arithmetic in a linear logic.
 % EXPECT: The fact in question: TERM

diff --git a/test/regress/regress0/expect/scrub.09.p b/test/regress/regress0/expect/scrub.09.p
index 0297b115561314d24546210a70a6544d52510cd4..20cdf2c18eba3f6300b12ff274d2379a6327fb69 100644 (file)
--- a/test/regress/regress0/expect/scrub.09.p
+++ b/test/regress/regress0/expect/scrub.09.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE: 
+% COMMAND-LINE: --force-logic=UFLIA
 % SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 % EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 % EXPECT: The fact in question: TERM