Mark #distinctBits as "no-evaluators" (#632)

runtimeverification · May 16, 2024 · b104b92 · b104b92
1 parent 954bdbc
commit b104b92
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.51
+0.1.52
diff --git a/pykwasm/pyproject.toml b/pykwasm/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pykwasm"
-version = "0.1.51"
+version = "0.1.52"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md
@@ -288,7 +288,7 @@ Bounds on `#getRange`:
     rule #getRange(_, _, WIDTH) <<Int SHIFT <Int MAX => true requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX                          [simplification]
     rule VAL1 +Int VAL2                     <Int MAX => true requires VAL1 <Int MAX andBool VAL2 <Int MAX andBool #distinctBits(VAL1, VAL2) [simplification]
 
-    syntax Bool ::= #distinctBits ( Int , Int ) [function]
+    syntax Bool ::= #distinctBits ( Int , Int ) [function, no-evaluators]
  // ------------------------------------------------------
     rule #distinctBits(#getRange(_, _, WIDTH), #getRange(_, _, _) <<Int SHIFT) => true requires WIDTH *Int 8 <=Int SHIFT
       [simplification]