From 367cc4b77f4ae283790556b848be31390a8e22c6 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sat, 22 Apr 2017 13:36:09 -0400 Subject: [PATCH] check result of unsat core validation --- src/smt/smt_context.cpp | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 225a0d58d..32fb492ad 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3281,13 +3281,21 @@ namespace smt { TRACE("after_internalization", display(tout);); if (inconsistent()) { VERIFY(!resolve_conflict()); // build the proof - mk_unsat_core(); - r = l_false; + lbool result = mk_unsat_core(); + if (result == l_undef) { + r = l_undef; + } else { + r = l_false; + } } else { r = search(); - if (r == l_false) - mk_unsat_core(); + if (r == l_false) { + lbool result = mk_unsat_core(); + if (result == l_undef) { + r = l_undef; + } + } } } }