From: Clark Barrett <barrett@cs.nyu.edu>
Date: Sat, 10 Nov 2012 04:34:34 +0000 (+0000)
Subject: Finally tracked down problems in regressions and fuzz results (this also
X-Git-Tag: cvc5-1.0.0~7628
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=71b15fb7279c9e52b1b2b538887db2c1a44a8fa7;p=cvc5.git

Finally tracked down problems in regressions and fuzz results (this also
explains why my build was giving different answers from Dejan's build).
Problem was that if you run:

cvc4 --check-models foo.smt

it would fail, but if you run

cvc4 --check-models --produce-models foo.smt

it would succeed.  Even though produce-models is supposed to be automatically
set when you set check-models, it seems this was happening too late.  Fixed by
removing any distinction between produce-models and check-models in the
heuristic setting code.  Kind of ugly though.

Also, disable models if nonlinear arithmetic is on.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index df9526571..761fe3b8c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -744,7 +744,7 @@ void SmtEngine::setLogicInternal() throw() {
   if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) {
     //    bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
     //    bool uncSimp = false && !qf_sat && !options::incrementalSolving();
-    bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() &&
+    bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() && !options::produceModels() && !options::checkModels() &&
       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
     options::unconstrainedSimp.set(uncSimp);
@@ -883,10 +883,23 @@ void SmtEngine::setLogicInternal() throw() {
   }
 
   // For now, these array theory optimizations do not support model-building
-  if (options::produceModels()) {
+  if (options::produceModels() || options::checkModels()) {
     options::arraysOptimizeLinear.set(false);
     options::arraysLazyRIntro1.set(false);
   }
+
+  // Non-linear arithmetic does not support models
+  if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+      !d_logic.isLinear()) {
+    if (options::produceModels()) {
+      Notice() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl;
+      setOption("produce-models", SExpr("false"));
+    }
+    if (options::checkModels()) {
+      Notice() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl;
+      setOption("check-models", SExpr("false"));
+    }    
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)