fix #6194

Z3Prover · Jul 27, 2022 · 8551b21 · 8551b21
1 parent b6c80e8
commit 8551b21
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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);