From f7e0adeae28bae50632edef3ed2325df67a7ee7a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Mar 2018 00:45:38 -0500 Subject: [PATCH] Check model only when sat (#1694) --- src/smt/smt_engine.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index d3489b301..8450307db 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4866,9 +4866,10 @@ Result SmtEngine::checkSatisfiability(const vector& assumptions, // Check that SAT results generate a model correctly. if(options::checkModels()) { - if(r.asSatisfiabilityResult().isSat() == Result::SAT || - (r.isUnknown() && r.whyUnknown() == Result::INCOMPLETE) ){ - checkModel(/* hard failure iff */ ! r.isUnknown()); + // TODO (#1693) check model when unknown result? + if (r.asSatisfiabilityResult().isSat() == Result::SAT) + { + checkModel(); } } // Check that UNSAT results generate a proof correctly. -- 2.30.2