From 32f3bd17fb5ef7e7195d69351baf48b0a6466c08 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Oct 2015 14:30:54 -0700 Subject: [PATCH] adding translation routine to context to address enhancement request #209 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index bd1bfc52d..6149dc671 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -152,7 +152,7 @@ namespace smt { asserted_formulas& src_af = m_asserted_formulas; asserted_formulas& dst_af = new_ctx->m_asserted_formulas; - SASSERT(m_base_lvl == 0); // please don't clone me + SASSERT(m_base_lvl == 0); SASSERT(src_af.get_qhead() == src_af.get_num_formulas()); // should be the same. // Copy asserted formulas. @@ -209,7 +209,7 @@ namespace smt { else if (e = m_bool_var2expr.get(lit.var(), 0)) { result = ::translate(e, m_manager, m); if (lit.sign()) { - result = dst.get_manager().mk_not(result); + result = m.mk_not(result); } } return result;