adding definedness constraints for ecrec

runtimeverification · Aug 10, 2023 · a35b70e · a35b70e
1 parent 3279e4f
commit a35b70e
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k
@@ -20,6 +20,12 @@ module VERIFICATION-COMMON
     rule 0 <=Int #asWord(#ecrec(_   , _   , _   , _   ))                  => true                                                      [simplification]
     rule         #asWord(#ecrec(_   , _   , _   , _   )) <=Int maxUInt160 => true                                                      [simplification]
 
+    rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top
+     requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
+
+    rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top
+     requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
+
 endmodule
 
 module VERIFICATION