mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

skip expensive equality rewriting of Booleans

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-20 10:31:10 +02:00
parent 10b611b3ba
commit 4d184fe65d
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -649,7 +649,7 @@ class solve_eqs_tactic : public tactic {
for (unsigned i = 0; i < args.size(); ++i) {
pr = nullptr;
expr* arg = args.get(i), *lhs = nullptr, *rhs = nullptr;
if (m().is_eq(arg, lhs, rhs)) {
if (m().is_eq(arg, lhs, rhs) && !m().is_bool(lhs)) {
if (trivial_solve1(lhs, rhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
insert_solution(g, idx, arg, var, def, pr);
}