mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix overlap detection internalization

Browse source
This commit is contained in:
Murphy Berzish 2017-05-03 17:46:06 -04:00
parent ab4fbe40b6
commit c2b5e8cfda
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -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