From b7111874c9b3fefea7b291d86309427793dc36ef Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Tue, 24 Dec 2024 18:30:46 +0000
Subject: [PATCH] cex reducer: skip testing implied constraints

---
 tools/transform.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tools/transform.cpp b/tools/transform.cpp
index fbb9c89bc..f4f014a99 100644
--- 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);