From 086ea7867ec487ba263095fc7f797ebaf530db02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 14 Aug 2017 12:52:25 -0700 Subject: [PATCH] another stab at #989 Signed-off-by: Nikolaj Bjorner --- scripts/update_api.py | 2 +- src/smt/smt_context.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 7c9f553cb..4000b3da2 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -322,7 +322,7 @@ def mk_py_wrappers(): display_args(num) core_py.write("):\n") core_py.write(" _lib = lib()\n") - core_py.write(" if _lib.%s is None:\n" % name) + core_py.write(" if _lib is None or _lib.%s is None:\n" % name) core_py.write(" return\n") if result != VOID: core_py.write(" r = _lib.%s(" % name) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 42e382790..daa408161 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3290,11 +3290,11 @@ namespace smt { internalize_assertions(); lbool r = l_undef; + TRACE("before_search", display(tout);); if (m_asserted_formulas.inconsistent()) { r = l_false; } else { - TRACE("after_internalization", display(tout);); if (inconsistent()) { VERIFY(!resolve_conflict()); // build the proof r = l_false;