old Z3 encoding experiment: marked with [smtlib] #symEcrec and `Int "…

…:" WordStack`.
runtimeverification · Dec 5, 2018 · 7e2e47a · 7e2e47a
1 parent 5d3bbb6
commit 7e2e47a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/data.md b/data.md
@@ -403,7 +403,7 @@ A cons-list is used for the EVM wordstack.
 
 ```k
     syntax WordStack [flatPredicate]
-    syntax WordStack ::= ".WordStack" | Int ":" WordStack
+    syntax WordStack ::= ".WordStack" | Int ":" WordStack [smtlib(ws)]
  // -----------------------------------------------------
 ```
 

diff --git a/evm-symbolic.md b/evm-symbolic.md
@@ -25,10 +25,10 @@ Symbolic result of ecrecover.
       requires notBool #isConcrete(DATA) andBool #sizeWordStack(DATA) ==Int 128 andBool #ecrecEmpty(DATA)
 
     //Symbolic wrapper over the argument of #ecrec, no implementation. 
-    syntax Int ::= #symEcrec ( WordStack )   [function]
+    syntax Int ::= #symEcrec ( WordStack )   [function, smtlib(sym_ecrec)]
     
     //Symbolic predicate representing whether output of #ecrec is empty. No implementation.
-    syntax Bool ::= #ecrecEmpty( WordStack ) [function]
+    syntax Bool ::= #ecrecEmpty( WordStack ) [function, smtlib(ecrec_empty)]
 ```
 
 Split construct. Allows to force branching on arbitrary boolean expressions.