Regressions now checking models on unknown too. But quantifiers don't have to be...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 927b8fe6f52e008587ed005a984350f3d7ee3ef0..4fa8e53d8b2e9054db5021f14a10d40dddff7c00 100644 (file)
--- 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 b740e84860a7b287369f7f61a3be47e7afccc2b4..a67496514b4bdedcde034fc629eed10eb2fdea88 100755 (executable)
--- 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