From c2b5e8cfdafec22eaf7614bfc688566b1c09b42e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 3 May 2017 17:46:06 -0400 Subject: [PATCH] fix overlap detection internalization --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index be268ec5c..a26cb2ee2 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7305,7 +7305,7 @@ lbool theory_str::validate_unsat_core(expr_ref_vector & unsat_core) { bool assumptionFound = false; app * target_term = to_app(get_manager().mk_not(m_theoryStrOverlapAssumption_term)); - internalize_term(target_term); + get_context().internalize(target_term, false); for (unsigned i = 0; i < unsat_core.size(); ++i) { app * core_term = to_app(unsat_core.get(i)); // not sure if this is the correct way to compare terms in this context