Temporary roll back of set var axioms
@@ -423,16 +423,22 @@ module INT-SYMBOLIC [symbolic, kore]
* Definability conditions for _/Int_ and _%Int_
*/
+ rule #Ceil(I1:Int /Int I2:Int) => {(I2 =/=Int 0) #Equals true} [anywhere]
+/* TODO(traiansf): The rule above should change to the version below once we implement set variables.
rule
#Ceil(@I1:Int /Int @I2:Int)
=>
{(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2)
[anywhere]
+*/
+ rule #Ceil(I1:Int %Int I2:Int) => {(I2 =/=Int 0) #Equals true} [anywhere]
+/* TODO(traiansf): The rule above should change to the version below once we implement set variables.
rule
#Ceil(@I1:Int %Int @I2:Int)
=>
{(@I2 =/=Int 0) #Equals true} #And #Ceil(@I1) #And #Ceil(@I2)
[anywhere]
+*/
endmodule
module INT
