mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

finite model fix

Browse source
This commit is contained in:
Murphy Berzish 2017-01-16 21:42:11 -05:00
parent 0af834421f
commit 794e210958
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_str.cpp
View file

@ -6673,6 +6673,12 @@ void theory_str::finite_model_test(expr * testvar, expr * str) {
ptr_vector<expr> & vars = finite_model_test_varlists[testvar]; ptr_vector<expr> & vars = finite_model_test_varlists[testvar];
for (ptr_vector<expr>::iterator it = vars.begin(); it != vars.end(); ++it) { for (ptr_vector<expr>::iterator it = vars.begin(); it != vars.end(); ++it) {
expr * v = *it; expr * v = *it;
bool v_has_eqc = false;
get_eqc_value(v, v_has_eqc);
if (v_has_eqc) {
TRACE("t_str_detail", tout << "variable " << mk_pp(v,m) << " already equivalent to a string constant" << std::endl;);
continue;
}
// check for any sort of existing length tester we might interfere with // check for any sort of existing length tester we might interfere with
if (m_params.m_UseBinarySearch) { if (m_params.m_UseBinarySearch) {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
@ -6763,8 +6769,8 @@ void theory_str::finite_model_test(expr * testvar, expr * str) {
expr_ref implRhs(mk_and(andList), m); expr_ref implRhs(mk_and(andList), m);
assert_implication(implLhs, implRhs); assert_implication(implLhs, implRhs);
} else { } else {
// TODO figure out this case TRACE("t_str_detail", tout << "already found existing length testers for " << mk_pp(v, m) << std::endl;);
NOT_IMPLEMENTED_YET(); continue;
} }
} }
} // foreach (v in vars) } // foreach (v in vars)