From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 19 Jul 2013 17:24:29 +0000 (-0400)
Subject: Regressions now checking models on unknown too.  But quantifiers don't have to be... 
X-Git-Tag: cvc5-1.0.0~7287^2~44
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc3db83a6856016c9c838fbabdd29f962aa60769;p=cvc5.git

Regressions now checking models on unknown too.  But quantifiers don't have to be simplified by check-model in that case.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 927b8fe6f..4fa8e53d8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3571,7 +3571,7 @@ void SmtEngine::checkModel(bool hardFailure) {
     // but don't show up in our substitution map above.
     n = m->getValue(n);
     Notice() << "SmtEngine::checkModel(): -- model-substitutes to " << n << endl;
-    AlwaysAssert(n.isConst() || n.getKind() == kind::LAMBDA);
+    AlwaysAssert(!hardFailure || n.isConst() || n.getKind() == kind::LAMBDA);
 
     // The result should be == true.
     if(n != NodeManager::currentNM()->mkConst(true)) {
diff --git a/test/regress/run_regression b/test/regress/run_regression
index b740e8486..a67496514 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -213,7 +213,7 @@ else
   echo "$expected_output" >"$expoutfile"
 fi
 check_models=false
-if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null; then
+if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then
   if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null &&
      ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models' &>/dev/null; then
     # later on, we'll run another test with --check-models on