From 4d184fe65d5afdb58611b9c537d597f59564c926 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Feb 2022 10:31:10 +0200 Subject: [PATCH] skip expensive equality rewriting of Booleans --- src/tactic/core/solve_eqs_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index a73fe88b6..8d4130a89 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -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); }