Fix div0 for reals

soarlab · Mar 11, 2020 · 0a6a72a · 0a6a72a
1 parent 8e931fb
commit 0a6a72a
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/pysmt/rewritings.py b/pysmt/rewritings.py
@@ -1397,9 +1397,7 @@ def walk_ufxp_div(self, formula, args, **kwargs):
         rm = args[1]
         left = args[2]
         right = args[3]
-        return self.mgr.Ite(self.mgr.Equals(right, self.mgr.Real(Fraction(0))),
-                            self.mgr.FreshSymbol(types.REAL),
-                            self.process_real_round(self.mgr.Div(left,right,reduce_const=False),om,rm,0,total_width,frac_width))
+        return self.process_real_round(self.mgr.Div(left,right,reduce_const=False),om,rm,0,total_width,frac_width)
 
 
     def walk_sfxp_div(self, formula, args, **kwargs):
@@ -1410,9 +1408,7 @@ def walk_sfxp_div(self, formula, args, **kwargs):
         rm = args[1]
         left = args[2]
         right = args[3]
-        return self.mgr.Ite(self.mgr.Equals(right, self.mgr.Real(Fraction(0))),
-                            self.mgr.FreshSymbol(types.REAL),
-                            self.process_real_round(self.mgr.Div(left,right,reduce_const=False),om,rm,1,total_width,frac_width))
+        return self.process_real_round(self.mgr.Div(left,right,reduce_const=False),om,rm,1,total_width,frac_width)
 
     def walk_symbol(self, formula, **kwargs):
         ty = self.env.stc.get_type(formula)

diff --git a/pysmt/smtlib/printers.py b/pysmt/smtlib/printers.py
@@ -60,6 +60,7 @@ def walk_le(self, formula): return self.walk_nary(formula, "<=")
     def walk_lt(self, formula): return self.walk_nary(formula, "<")
     def walk_ite(self, formula): return self.walk_nary(formula, "ite")
     def walk_toreal(self, formula): return self.walk_nary(formula, "to_real")
+    def walk_realtoint(self, formula): return self.walk_nary(formula, "to_int")
     def walk_div(self, formula): return self.walk_nary(formula, "/")
     def walk_pow(self, formula): return self.walk_nary(formula, "pow")
     def walk_bv_and(self, formula): return self.walk_nary(formula, "bvand")
@@ -362,6 +363,9 @@ def walk_ite(self, formula, args):
 
     def walk_toreal(self, formula, args):
         return self.walk_nary(formula, args, "to_real")
+
+    def walk_realtoint(self, formula, args):
+        return self.walk_nary(formula, args, "to_int")
 
     def walk_div(self, formula, args):
         return self.walk_nary(formula, args, "/")