From dd6bbf3ef3ce7ccfc39aaaa8b54ec8b85237cd45 Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Sat, 15 Jul 2023 12:41:10 +0300
Subject: [PATCH] Make checkNoPayment work in symbolic execution (#115)

---
 vmhooks/baseOps.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/vmhooks/baseOps.md b/vmhooks/baseOps.md
index 46599e0c..25a66928 100644
--- a/vmhooks/baseOps.md
+++ b/vmhooks/baseOps.md
@@ -209,8 +209,8 @@ module BASEOPS
     rule [checkNoPayment-pass]:
         <instrs> hostCall("env", "checkNoPayment", [ .ValTypes ] -> [ .ValTypes ]) => . ... </instrs>
         <callValue> VAL </callValue>
-        <esdtTransfers> .List </esdtTransfers>
-      requires VAL <=Int 0
+        <esdtTransfers> T:List </esdtTransfers>
+      requires VAL <=Int 0 andBool size(T) ==K 0
 
     rule [checkNoPayment-fail-egld]:
         <instrs> hostCall("env", "checkNoPayment", [ .ValTypes ] -> [ .ValTypes ]) 
@@ -224,8 +224,8 @@ module BASEOPS
               => #throwException(ExecutionFailed, "function does not accept ESDT payment") ... 
         </instrs>
         <callValue> VAL </callValue>
-        <esdtTransfers> ListItem(_) ... </esdtTransfers>
-      requires VAL <=Int 0
+        <esdtTransfers> T:List </esdtTransfers>
+      requires VAL <=Int 0 andBool 0 <Int size(T)
 
     // extern int32_t getESDTTokenName(void *context, int32_t resultOffset);
     rule [getESDTTokenName]: