cex reducer: skip testing implied constraints

AliveToolkit · Dec 24, 2024 · b711187 · b711187
1 parent c5ddf97
commit b711187
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/tools/transform.cpp b/tools/transform.cpp
@@ -168,6 +168,9 @@ static bool error(Errors &errs, State &src_state, State &tgt_state,
   optional<Result> newr;
 
   auto try_reduce = [&](const expr &e) {
+    if (e.isTrue())
+      return true;
+
     bool ok = false;
     {
       SolverPush push(solver);