From a2aab76c2264d597198bfbe8c55fb9f3687e6de4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 Dec 2019 11:02:25 +0300 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- src/qe/qsat.cpp | 4 +++- src/smt/theory_diff_logic_def.h | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 7fbb787fc..d242e0e11 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -1076,7 +1076,9 @@ namespace qe { bool validate_assumptions(model& mdl, expr_ref_vector const& core) { for (expr* c : core) { if (!mdl.is_true(c)) { - TRACE("qe", tout << "component of core is not true: " << mk_pp(c, m) << "\n";); + TRACE("qe", tout << "component of core is not true: " << mk_pp(c, m) << "\n"; + tout << mdl << "\n"; + ); return false; } } diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index d85ba9da1..31bdf30fd 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -367,7 +367,9 @@ final_check_status theory_diff_logic::final_check_eh() { for (enode* n : get_context().enodes()) { family_id fid = n->get_owner()->get_family_id(); if (fid != get_family_id() && - fid != get_manager().get_basic_family_id()) { + fid != get_manager().get_basic_family_id() && + !is_uninterp_const(n->get_owner())) { + TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << "\n";); return FC_GIVEUP; } }