From 56562a725d7591062df279626fdfe5b26797a43d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Dec 2013 19:24:20 -0600 Subject: [PATCH] fixing bugs Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 448086c6d..26fb655a9 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1090,10 +1090,8 @@ namespace smt { ast_manager& m = get_manager(); context& ctx = get_context(); std::ostringstream strm; - expr_ref b(m); strm << val << " <= v" << v; - b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); - SASSERT(m_unassigned_atoms.size() == m_var_occs.size()); + expr* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort()); if (!ctx.b_internalized(b)) { bool_var bv = ctx.mk_bool_var(b); ctx.set_var_theory(bv, get_id());