Multi-solution now

src/EVM.hs

@@ -2988,7 +2988,7 @@ instance VMOps Symbolic where
 
   manySolutions ewordExpr isAddr continue = do
     pathconds <- use #constraints
-    query $ PleaseGetSol ewordExpr isAddr pathconds $ \case
+    query $ PleaseGetSols ewordExpr isAddr pathconds $ \case
       Just concVals -> do
         assign #result Nothing
         case (length concVals) of

src/EVM/Fetch.hs

@@ -214,7 +214,7 @@ oracle solvers info q = do
          -- Is is possible to satisfy the condition?
          continue <$> checkBranch solvers (branchcondition ./= (Lit 0)) pathconds
 
-    PleaseGetSol symExpr isAddr pathconditions continue -> do
+    PleaseGetSols symExpr isAddr pathconditions continue -> do
          let pathconds = foldl' PAnd (PBool True) pathconditions
          continue <$> getSolutions solvers symExpr isAddr pathconds
 

src/EVM/Types.hs

@@ -594,7 +594,7 @@ data Query t s where
   PleaseFetchContract :: Addr -> BaseState -> (Contract -> EVM t s ()) -> Query t s
   PleaseFetchSlot     :: Addr -> W256 -> (W256 -> EVM t s ()) -> Query t s
   PleaseAskSMT        :: Expr EWord -> [Prop] -> (BranchCondition -> EVM Symbolic s ()) -> Query Symbolic s
-  PleaseGetSol        :: Expr EWord -> Bool -> [Prop] -> (Maybe [W256] -> EVM Symbolic s ()) -> Query Symbolic s
+  PleaseGetSols       :: Expr EWord -> Bool -> [Prop] -> (Maybe [W256] -> EVM Symbolic s ()) -> Query Symbolic s
   PleaseDoFFI         :: [String] -> Map String String -> (ByteString -> EVM t s ()) -> Query t s
   PleaseReadEnv       :: String -> (String -> EVM t s ()) -> Query t s
 
@@ -618,7 +618,7 @@ instance Show (Query t s) where
       (("<EVM.Query: ask SMT about "
         ++ show condition ++ " in context "
         ++ show constraints ++ ">") ++)
-    PleaseGetSol expr isAddr constraints _ ->
+    PleaseGetSols expr isAddr constraints _ ->
       (("<EVM.Query: ask SMT "
         ++ if isAddr then "for address " else "for value "
         ++ "to get W256 for expression "