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

temporarily remove finite model finding from theory_str

Browse source
This commit is contained in:
Murphy Berzish 2017-02-07 17:14:11 -05:00
parent 55cb440aae
commit c456795acd
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_str.cpp
View file

@ -6968,6 +6968,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) {
return; return;
} }
/* // temporarily disabled, we are borrowing these testers for something else
if (m_params.m_FiniteOverlapModels && !finite_model_test_varlists.empty()) { if (m_params.m_FiniteOverlapModels && !finite_model_test_varlists.empty()) {
// TODO NEXT // TODO NEXT
if (finite_model_test_varlists.contains(lhs)) { if (finite_model_test_varlists.contains(lhs)) {
@ -6976,6 +6977,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) {
finite_model_test(rhs, lhs); return; finite_model_test(rhs, lhs); return;
} }
} }
*/
if (free_var_attempt(lhs, rhs) || free_var_attempt(rhs, lhs)) { if (free_var_attempt(lhs, rhs) || free_var_attempt(rhs, lhs)) {
return; return;