Do not silently ignore mod over floats - fail instead

tautschnig · tautschnig · commit 959f61808805 · 2017-02-15T08:01:59.000Z
diff --git a/src/solvers/flattening/boolbv_mod.cpp b/src/solvers/flattening/boolbv_mod.cpp
@@ -22,10 +22,12 @@ Function: boolbvt::convert_mod
 
 bvt boolbvt::convert_mod(const mod_exprt &expr)
 {
+  #if 0
+  // TODO
   if(expr.type().id()==ID_floatbv)
   {
-    // TODO
   }
+  #endif
 
   if(expr.type().id()!=ID_unsignedbv &&
      expr.type().id()!=ID_signedbv)

Original file line number	Diff line number	Diff line change
`@@ -22,10 +22,12 @@ Function: boolbvt::convert_mod`
`22`	`22`
`23`	`23`	`bvt boolbvt::convert_mod(const mod_exprt &expr)`
`24`	`24`	`{`
	`25`	`+ #if 0`
	`26`	`+ // TODO`
`25`	`27`	`if(expr.type().id()==ID_floatbv)`
`26`	`28`	`{`
`27`		`- // TODO`
`28`	`29`	`}`
	`30`	`+ #endif`
`29`	`31`
`30`	`32`	`if(expr.type().id()!=ID_unsignedbv &&`
`31`	`33`	`expr.type().id()!=ID_signedbv)`