The branch node only needs to remember the positive condition.

use the sub-nodes of the branch to classify whether the execution is true or false

Author: butterunderflow

src/main/scala/wasm/StagedConcolicMiniWasm.scala

@@ -228,7 +228,7 @@ trait StagedWasmEvaluator extends SAIOps {
           ExploreTree.fillWithIfElse(cond.s, true)
           eval(thn, restK _, mkont, restK _ :: trail)(newCtx)
         } else {
-          ExploreTree.fillWithIfElse(cond.s.not, false)
+          ExploreTree.fillWithIfElse(cond.s, false)
           eval(els, restK _, mkont, restK _ :: trail)(newCtx)
         }
         ()
@@ -245,7 +245,7 @@ trait StagedWasmEvaluator extends SAIOps {
           trail(label)(newCtx)(mkont)
         } else {
           info(s"Continue")
-          ExploreTree.fillWithIfElse(cond.s.not, false)
+          ExploreTree.fillWithIfElse(cond.s, false)
           eval(rest, kont, mkont, trail)(newCtx)
         }
         ()