add definability condition for modInt
@@ -420,7 +420,7 @@ module INT-SYMBOLIC [symbolic, kore]
imports ML-SYNTAX
/**
- * Definability conditions for _/Int_ and _%Int_
+ * Definability conditions
*/
rule
@@ -428,11 +428,18 @@ module INT-SYMBOLIC [symbolic, kore]
=>
{(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2)
[anywhere]
+
rule
#Ceil(@I1:Int %Int @I2:Int)
=>
{(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2)
[anywhere]
+
+ rule
+ #Ceil(@I1:Int modInt @I2:Int)
+ =>
+ {(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2)
+ [anywhere]
endmodule
module INT
