diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 4b7da8b71..a1f0f9777 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -10430,6 +10430,9 @@ namespace smt { // iterate parents if (standAlone) { // I hope this works! + if (!ctx.e_internalized(freeVar)) { + ctx.internalize(freeVar, false); + } enode * e_freeVar = ctx.get_enode(freeVar); enode_vector::iterator it = e_freeVar->begin_parents(); for (; it != e_freeVar->end_parents(); ++it) {