From 8551b217ce69509041e82ad04541fd5d907aed42 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 Jul 2022 08:03:57 +0200
Subject: [PATCH] fix #6194

---
 src/smt/theory_lra.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 75f9cb99710..0b9f4c072f5 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1113,7 +1113,7 @@ class theory_lra::imp {
         }
         {
             scoped_trace_stream ts(th, dgez, neg);
-            mk_axiom( dgez, neg);                    
+            mk_axiom( dgez, neg);
         }
     }
 
@@ -1224,7 +1224,6 @@ class theory_lra::imp {
             return;
         }
         expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m);
-        ctx().get_rewriter()(mod_r);
         expr_ref eq_r(th.mk_eq_atom(mod_r, p), m);
         ctx().internalize(eq_r, false);
         literal eq = ctx().get_literal(eq_r);