From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 5 Jul 2017 21:55:20 +0000 (-0500)
Subject: Fix for logic info, update regressions. Update casc tfa script.
X-Git-Tag: cvc5-1.0.0~5745
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94e6dfdb96d8ca3558789b51384349f66415c540;p=cvc5.git

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 05062bf5c..74147e529 100644
--- 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 6f519c15f..3a89ca048 100644
--- 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 896149334..2656c71b3 100644
--- 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 0297b1155..20cdf2c18 100644
--- 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