mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix regression regex-020

Browse source
This commit is contained in:
Murphy Berzish 2016-09-20 00:14:38 -04:00
parent 9615b191de
commit f1d7ffcdce
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_str.cpp
View file

@ -7641,9 +7641,9 @@ final_check_status theory_str::final_check_eh() {
get_eqc_value(*it, has_eqc_value); get_eqc_value(*it, has_eqc_value);
if (!has_eqc_value) { if (!has_eqc_value) {
// if this is an internal variable, it can be ignored...I think // if this is an internal variable, it can be ignored...I think
if (internal_variable_set.find(*it) != internal_variable_set.end()) { if (internal_variable_set.find(*it) != internal_variable_set.end() || regex_variable_set.find(*it) != regex_variable_set.end()) {
TRACE("t_str_detail", tout << "WARNING: free internal variable " << mk_ismt2_pp(*it, m) << std::endl;); TRACE("t_str_detail", tout << "WARNING: free internal variable " << mk_ismt2_pp(*it, m) << std::endl;);
unused_internal_variables.insert(*it); //unused_internal_variables.insert(*it);
} else { } else {
needToAssignFreeVars = true; needToAssignFreeVars = true;
free_variables.insert(*it); free_variables.insert(*it);