From af3ca1fc7ba79cca1541a1e074c06bd2a93fad0f Mon Sep 17 00:00:00 2001
From: Niels Saurer <me@nielssaurer.com>
Date: Sun, 21 Nov 2021 17:03:43 +0100
Subject: [PATCH] Fix assume! directive in SE

---
 src/se.rs | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/se.rs b/src/se.rs
index 509ee0f..4faabe5 100644
--- a/src/se.rs
+++ b/src/se.rs
@@ -541,14 +541,15 @@ impl SymbolicExecutor {
             }
             Stmt::While { .. } => panic!("While should have been removed in loop bounding"),
             Stmt::Call(name, args) if name.as_str() == "assume!" => {
-                // TODO: Will need to handle Stmt::Call in the future when arrays are supported.
-                // TODO: that's now. Do it.
-                let new_pct = Expr::BinOp(
-                    WL::no_loc(BinOpcode::And),
-                    Box::new(WL::no_loc(pct.clone())),
-                    Box::new(args[0].clone()),
-                );
-                return vec![(store.clone(), new_pct, sym_heap.clone(), ret_val.clone())];
+                // assume! has one arg
+                store.symbolize(self, &args[0], pct, sym_heap).into_iter().map(|(sym_arg, pct, sym_heap)| {
+                    let new_pct = Expr::BinOp(
+                        WL::no_loc(BinOpcode::And),
+                        Box::new(WL::no_loc(pct)),
+                        Box::new(WL::no_loc(sym_arg.into_expr().unwrap())),
+                    );
+                    (store.clone(), new_pct, sym_heap, ret_val.clone())
+                }).collect()
             }
             Stmt::Call(name, args) => {
                 // Built-ins' only side-effects are that they might change the symbolic heap.