From bfd0d07e2c265b11fe35e067305bc3a7da75d5bb Mon Sep 17 00:00:00 2001 From: ZhuXiaoran07 Date: Mon, 11 Sep 2017 16:18:02 -0500 Subject: [PATCH] add "smtlib" attribute to the definition of "in_keys" (for the verification of EVM) --- k-distribution/include/builtin/domains.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k index 11b28ad6c7..d2756c19c1 100644 --- a/k-distribution/include/builtin/domains.k +++ b/k-distribution/include/builtin/domains.k @@ -69,7 +69,7 @@ module MAP /*@ Get a Set consisting of all keys in the Map:*/ syntax Set ::= keys(Map) [function, hook(MAP.keys), relativeHook(_Map_.keys)] - syntax Bool ::= K "in_keys" "(" Map ")" [function, hook(MAP.in_keys)] + syntax Bool ::= K "in_keys" "(" Map ")" [function, hook(MAP.in_keys), smtlib(inkeys)] /*@ Get a List consisting of all values in the Map: */ syntax List ::= values(Map) [function, hook(MAP.values)]