diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index 51084f809..5bb91a49e 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -1201,9 +1201,12 @@ public:
         ast t = arg(my_con,0);
         ast c = arg(my_con,1);
         ast d = gcd_of_coefficients(t);
+        /*
         t = z3_simplify(mk_idiv(t,d));
         c = z3_simplify(mk_idiv(c,d));
         ast cut_con = make(op(my_con),t,c);
+        */
+        ast cut_con = con;
         return iproof->make_cut_rule(my_con,d,cut_con,res);
     }