From f059b5e16b4aff8e6cf5e340af1621e3a663fee2 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at>
Date: Tue, 7 Mar 2023 15:53:32 +0100
Subject: [PATCH] Leftover debug return

---
 src/math/polysat/saturation.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index f682fae09..2c4f58421 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -228,7 +228,6 @@ namespace polysat {
     bool saturation::try_op(pvar v, signed_constraint c, conflict& core) {
         SASSERT(c->is_op());
         SASSERT(c.is_positive());
-        return false;
         op_constraint* op = ((op_constraint*)c.get());
         clause_ref correction = op->produce_lemma(s, s.get_assignment(), c.is_positive());
         if (correction) {