Fix the SIGNEXTEND kore/haskell backend test. (#434)

* Fix the SIGNEXTEND kore/haskell backend test. * data: formatting
runtimeverification · Aug 13, 2019 · ea55a76 · ea55a76
1 parent b31f51b
commit ea55a76
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/data.md b/data.md
@@ -373,9 +373,9 @@ Bitwise logical operators are lifted from the integer versions.
 ```k
     syntax Int ::= signextend( Int , Int ) [function]
  // -------------------------------------------------
-    rule signextend(N, W) => W requires N >=Int 32 orBool N <Int 0
-    rule signextend(N, W) => chop( (#nBytes(31 -Int N) <<Byte (N +Int 1)) |Int W ) requires N <Int 32 andBool N >=Int 0 andBool         word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W))
-    rule signextend(N, W) => chop( #nBytes(N +Int 1)                      &Int W ) requires N <Int 32 andBool N >=Int 0 andBool notBool word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W))
+    rule signextend(N, W) => W requires N >=Int 32 orBool N <Int 0 [concrete]
+    rule signextend(N, W) => chop( (#nBytes(31 -Int N) <<Byte (N +Int 1)) |Int W ) requires N <Int 32 andBool N >=Int 0 andBool         word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W))         [concrete]
+    rule signextend(N, W) => chop( #nBytes(N +Int 1)                      &Int W ) requires N <Int 32 andBool N >=Int 0 andBool notBool word2Bool(bit(256 -Int (8 *Int (N +Int 1)), W)) [concrete]
 ```
 
 -   `keccak` serves as a wrapper around the `Keccak256` in `KRYPTO`.