diff --git a/benchmarks/wasm/call_indirect_test.1.wat b/benchmarks/wasm/call_indirect_test.1.wat
new file mode 100644
index 000000000..070224ce3
--- /dev/null
+++ b/benchmarks/wasm/call_indirect_test.1.wat
@@ -0,0 +1,38 @@
+(module
+  (type (;0;) (func (param i32) (result i32)))
+  (type (;1;) (func (param i32 i32) (result i32)))
+  (type (;2;) (func (result i32)))
+  (func (;0;) (type 0) (param i32) (result i32)
+    local.get 0
+    i32.const 1
+    i32.add)
+  (func (;1;) (type 0) (param i32) (result i32)
+    local.get 0
+    i32.const 2
+    i32.mul)
+  (func (;2;) (type 0) (param i32) (result i32)
+    local.get 0
+    i32.const 3
+    i32.sub)
+  (func (;3;) (type 1) (param i32 i32) (result i32)
+    local.get 1
+    local.get 0
+    call_indirect (type 0))
+  (func (;4;) (type 2) (result i32)
+    ;; (1 + 10) + (2 * 10) + (10 - 3) = 38
+    i32.const 1000
+    i32.const 10
+    call 3
+    i32.const 1001
+    i32.const 10
+    call 3
+    i32.add
+    i32.const 1002
+    i32.const 10
+    call 3
+    i32.add)
+  (table (;0;) 4 funcref)
+  (export "run" (func 4))
+  (export "dispatch" (func 3))
+  (elem (;0;) (i32.const 1000) func 0 1 2)
+  (start 4))
diff --git a/benchmarks/wasm/call_indirect_test.wat b/benchmarks/wasm/call_indirect_test.wat
index e38f4b97d..d5a119ada 100644
--- a/benchmarks/wasm/call_indirect_test.wat
+++ b/benchmarks/wasm/call_indirect_test.wat
@@ -3,9 +3,6 @@
   (type (;1;) (func (param i32 i32) (result i32)))
   (type (;2;) (func (result i32)))
   (func (;0;) (type 0) (param i32) (result i32)
-    (local i32 i32 i32 i32 i32)
-    local.get 3
-    drop
     local.get 0
     i32.const 1
     i32.add)
@@ -13,16 +10,29 @@
     local.get 0
     i32.const 2
     i32.mul)
-  (func (;2;) (type 1) (param i32 i32) (result i32)
+  (func (;2;) (type 0) (param i32) (result i32)
+    local.get 0
+    i32.const 3
+    i32.sub)
+  (func (;3;) (type 1) (param i32 i32) (result i32)
     local.get 1
     local.get 0
     call_indirect (type 0))
-  (func (;3;) (type 2) (result i32)
+  (func (;4;) (type 2) (result i32)
+    ;; (1 + 10) + (2 * 10) + (10 - 3) = 38
     i32.const 0
-    i32.const 41
-    call 2)
-  (table (;0;) 2 funcref)
-  (export "run" (func 3))
-  (export "dispatch" (func 2))
-  (elem (;0;) (i32.const 0) func 0 1)
-  (start 3))
+    i32.const 10
+    call 3
+    i32.const 1
+    i32.const 10
+    call 3
+    i32.add
+    i32.const 2
+    i32.const 10
+    call 3
+    i32.add)
+  (table (;0;) 3 funcref)
+  (export "run" (func 4))
+  (export "dispatch" (func 3))
+  (elem (;0;) (i32.const 0) func 0 1 2)
+  (start 4))
diff --git a/benchmarks/wasm/fp_ops.wat b/benchmarks/wasm/fp_ops.wat
index 17fdaf1c7..3c994ccef 100644
--- a/benchmarks/wasm/fp_ops.wat
+++ b/benchmarks/wasm/fp_ops.wat
@@ -15,6 +15,16 @@
     f64.const 0x1p-1 (;=0.5;)
     local.set 3
     local.get 0
+    f32.abs
+    f32.const 0x1.cp+1 (;=3.5;)
+    f32.eq
+    call 0
+    local.get 2
+    f64.abs
+    f64.const 0x1.48p+3 (;=10.25;)
+    f64.eq
+    call 0
+    local.get 0
     local.get 1
     f32.add
     f32.const 0x1.6p+2 (;=5.5;)
@@ -139,6 +149,18 @@
     f64.convert_i64_s
     f64.const -1.0
     f64.eq
+    call 0
+
+    f32.const 3.75
+    i32.trunc_f32_s
+    i32.const 3
+    i32.eq
+    call 0
+
+    f32.const 3.75
+    i32.trunc_f32_u
+    i32.const 3
+    i32.eq
     call 0)
 
   ;; symbolic branch guard for f32
diff --git a/headers/wasm/concolic_driver.hpp b/headers/wasm/concolic_driver.hpp
index fb8ffb4e9..0bd4ca3a2 100644
--- a/headers/wasm/concolic_driver.hpp
+++ b/headers/wasm/concolic_driver.hpp
@@ -86,6 +86,7 @@ class DefaultPathPicker : public PathPicker {
       : PathPicker(unexplored_paths, visited) {}
 
   std::optional<PathFrontier> pick_path() override {
+    ManagedTimer timer(TimeProfileKind::SOLVER_TOTAL);
     NodeBox *node = unexplored_paths.back();
     unexplored_paths.pop_back();
 
@@ -102,7 +103,6 @@ class DefaultPathPicker : public PathPicker {
 
     std::optional<QueryResult> result;
     {
-      ManagedTimer timer(TimeProfileKind::SOLVER_TOTAL);
       auto cond = node->collect_path_conds();
       result = solver.solve_path_conds(cond, true);
     }
@@ -196,7 +196,15 @@ inline void ConcolicDriver::main_exploration_loop() {
       GENSYM_INFO("Now execute the program with symbolic environment: ");
       GENSYM_INFO(SymEnv.to_string());
       auto snapshot = dynamic_cast<SnapshotNode *>(node->node.get());
+      if (snapshot && PROFILE_SNAPSHOT) {
+        auto resume_cost = snapshot->cost_of_snapshot_resume();
+        auto restart_cost = snapshot->cost_of_restart();
+        Profile.record_snapshot_history(resume_cost, restart_cost);
+      }
       if (REUSE_SNAPSHOT && snapshot && snapshot->worth_to_reuse()) {
+        // If we enabled snapshot reuse and the current snapshot is worth to
+        // reuse, resume the execution from the snapshot with the model we got
+        // from SMT solver.
         assert(REUSE_SNAPSHOT);
         Profile.incr_fromsnapshot_count();
         auto snap = snapshot->get_snapshot();
@@ -223,6 +231,7 @@ inline void ConcolicDriver::main_exploration_loop() {
       GENSYM_INFO("Caught runtime error during execution");
       switch (EXPLORE_MODE) {
       case ExploreMode::EarlyExit:
+        GENSYM_INFO("Exiting exploration due to error...");
         return;
       case ExploreMode::ExitByCoverage:
         if (ExploreTree.all_branch_covered()) {
@@ -274,4 +283,4 @@ static void start_concolic_execution_with(
   std::quick_exit(0);
 }
 
-#endif // CONCOLIC_DRIVER_HPP
\ No newline at end of file
+#endif // CONCOLIC_DRIVER_HPP
diff --git a/headers/wasm/concrete_num.hpp b/headers/wasm/concrete_num.hpp
index 6a2eafc50..56e44d248 100644
--- a/headers/wasm/concrete_num.hpp
+++ b/headers/wasm/concrete_num.hpp
@@ -640,6 +640,48 @@ struct Num {
     return Num(static_cast<int32_t>(r_bits));
   }
 
+  inline Num trunc_f32_to_i32_s() const {
+    uint32_t bits = toUInt();
+    float value = f32_from_bits(bits);
+
+    if (std::isnan(value)) {
+      throw std::runtime_error("i32.trunc_f32_s: NaN");
+    }
+    if (std::isinf(value)) {
+      throw std::runtime_error("i32.trunc_f32_s: Infinity");
+    }
+    if (value < -2147483648.0f || value >= 2147483648.0f) {
+      throw std::runtime_error("i32.trunc_f32_s: Out of range");
+    }
+
+    float truncated = std::trunc(value);
+    int32_t result = static_cast<int32_t>(truncated);
+    Num res(result);
+    debug_print("i32.trunc_f32_s", *this, *this, res);
+    return res;
+  }
+
+  inline Num trunc_f32_to_i32_u() const {
+    uint32_t bits = toUInt();
+    float value = f32_from_bits(bits);
+
+    if (std::isnan(value)) {
+      throw std::runtime_error("i32.trunc_f32_u: NaN");
+    }
+    if (std::isinf(value)) {
+      throw std::runtime_error("i32.trunc_f32_u: Infinity");
+    }
+    if (value < 0.0f || value >= 4294967296.0f) {
+      throw std::runtime_error("i32.trunc_f32_u: Out of range");
+    }
+
+    float truncated = std::trunc(value);
+    uint32_t result = static_cast<uint32_t>(truncated);
+    Num res(static_cast<int32_t>(result));
+    debug_print("i32.trunc_f32_u", *this, *this, res);
+    return res;
+  }
+
   // f32.min / f32.max: follow wasm-ish semantics: if either is NaN, return NaN
   // (propagate)
   inline Num f32_min(const Num &other) const {
diff --git a/headers/wasm/concrete_rt.hpp b/headers/wasm/concrete_rt.hpp
index 3e54baac8..c102ffbed 100644
--- a/headers/wasm/concrete_rt.hpp
+++ b/headers/wasm/concrete_rt.hpp
@@ -11,6 +11,7 @@
 #include <cstdio>
 #include <iostream>
 #include <memory>
+#include <optional>
 #include <ostream>
 #include <string>
 #include <unistd.h>
@@ -50,7 +51,10 @@ class Stack_t {
 
   Num pop() {
     Profile.step(StepProfileKind::POP);
-    assert(count > 0 && "Stack underflow");
+    if (count <= 0) {
+      assert(false);
+      throw std::runtime_error("Stack underflow");
+    }
 #ifdef DEBUG
     printf("[Debug] popping a value %ld from stack, size of concrete stack is: "
            "%d\n",
@@ -261,11 +265,15 @@ struct Memory_t {
     reset();
   }
 
+  void assert_valid_range(int32_t addr, size_t width) const {
+    assert(addr >= 0);
+    assert(static_cast<size_t>(addr) + width <= memory.size());
+    GENSYM_ASSERT_ADDR_ALLOCATED(addr, width);
+  }
+
   int32_t loadInt(int32_t base, int32_t offset) {
     int32_t addr = base + offset;
-    if (!(addr + 3 < memory.size()) || addr < 0) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 4);
     int32_t result = 0;
     // Little-endian: lowest byte at lowest address
     for (int i = 0; i < 4; ++i) {
@@ -282,9 +290,7 @@ struct Memory_t {
 
   uint8_t loadByte(int32_t base, int32_t offset) {
     int32_t addr = base + offset;
-    if (!(addr < memory.size()) || addr < 0) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 1);
     return memory[addr];
   }
 
@@ -343,15 +349,14 @@ struct Memory_t {
     uint64_t b1 = static_cast<uint64_t>(loadByte(base, offset + 1));
     uint64_t b2 = static_cast<uint64_t>(loadByte(base, offset + 2));
     uint64_t b3 = static_cast<uint64_t>(loadByte(base, offset + 3));
-    uint32_t raw = static_cast<uint32_t>(b0 | (b1 << 8) | (b2 << 16) | (b3 << 24));
+    uint32_t raw =
+        static_cast<uint32_t>(b0 | (b1 << 8) | (b2 << 16) | (b3 << 24));
     return static_cast<int32_t>(raw);
   }
 
   int64_t loadLong(int32_t base, int32_t offset) {
     int32_t addr = base + offset;
-    if (!(addr + 7 < memory.size()) || addr < 0) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 8);
     int64_t result = 0;
     for (int i = 0; i < 8; ++i) {
       result |= static_cast<int64_t>(memory[addr + i]) << (8 * i);
@@ -361,10 +366,7 @@ struct Memory_t {
 
   std::monostate storeInt(int32_t base, int32_t offset, int32_t value) {
     int32_t addr = base + offset;
-    // Ensure we don't write out of bounds
-    if (!(addr + 3 < memory.size())) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 4);
     for (int i = 0; i < 4; ++i) {
       memory[addr + i] = static_cast<uint8_t>((value >> (8 * i)) & 0xFF);
     }
@@ -377,11 +379,10 @@ struct Memory_t {
 
   std::monostate storeLong(int32_t base, int32_t offset, int64_t value) {
     int32_t addr = base + offset;
-    if (!(addr + 7 < memory.size()) || addr < 0) {
-      throw std::runtime_error("Invalid memory access " + std::to_string(addr));
-    }
+    assert_valid_range(addr, 8);
     for (int i = 0; i < 8; ++i) {
-      memory[addr + i] = static_cast<uint8_t>((static_cast<uint64_t>(value) >> (8 * i)) & 0xFF);
+      memory[addr + i] = static_cast<uint8_t>(
+          (static_cast<uint64_t>(value) >> (8 * i)) & 0xFF);
     }
     return std::monostate{};
   }
@@ -419,7 +420,7 @@ struct Memory_t {
     std::cout << "[Debug] storing byte " << std::to_string(value)
               << " to memory at address " << addr << std::endl;
 #endif
-    assert(addr < memory.size());
+    assert_valid_range(addr, 1);
     memory[addr] = value;
     return std::monostate{};
   }
@@ -470,26 +471,44 @@ struct FuncTable_t {
   std::vector<Func_t> table;
 
   Func_t read(int32_t index) {
-    if (index < 0 || index >= table.size()) {
+    auto offset = index - start_index.value();
+    if (offset < 0 || offset >= table.size()) {
       throw std::runtime_error("Function table read out of bounds: " +
                                std::to_string(index));
     }
-    if (!table[index]) {
-      assert(false);
+    if (!table[offset]) {
+      std::cout << "Function table entry at index " << index
+                << " is empty or invalid" << std::endl;
+      assert(false && "Function table entry is empty or invalid");
       throw std::runtime_error("Function table entry at index " +
                                std::to_string(index) + " is empty or invalid");
     }
-    return table[index];
+    return table[offset];
   }
 
   std::monostate set(Num offset, int32_t index, Func_t func) {
+    if (start_index.has_value()) {
+      assert(offset.toInt() == start_index &&
+             "Currently only supporting one function table per module.");
+    } else {
+      start_index = offset.toInt();
+    }
     if (index < 0 || index >= table.size()) {
       throw std::runtime_error("Function table set out of bounds: " +
                                std::to_string(index));
     }
-    table[offset.toInt() + index] = func;
+    table[index] = func;
     return std::monostate{};
   }
+
+  std::monostate setStart(int32_t index) {
+    // set start index to be the function at index 0
+    start_index = index;
+    return std::monostate{};
+  }
+
+private:
+  std::optional<int32_t> start_index;
 };
 
 static FuncTable_t FuncTable;
diff --git a/headers/wasm/config.hpp b/headers/wasm/config.hpp
index 6b64cbafa..79790041d 100644
--- a/headers/wasm/config.hpp
+++ b/headers/wasm/config.hpp
@@ -37,6 +37,12 @@ const bool PROFILE_PATH_CONDS = true;
 const bool PROFILE_PATH_CONDS = false;
 #endif
 
+#ifdef ENABLE_PROFILE_SNAPSHOT
+const bool PROFILE_SNAPSHOT = true;
+#else
+const bool PROFILE_SNAPSHOT = false;
+#endif
+
 // This variable define when concolic execution will stop
 enum class ExploreMode {
   EarlyExit, // Stop at the first error encountered
@@ -79,4 +85,10 @@ static const bool ENABLE_COST_MODEL = true;
 static const bool ENABLE_COST_MODEL = false;
 #endif
 
-#endif // CONFIG_HPP
\ No newline at end of file
+#ifdef USE_SOFT_ASSERT
+static const bool SOFT_ASSERT = true;
+#else
+static const bool SOFT_ASSERT = false;
+#endif
+
+#endif // CONFIG_HPP
diff --git a/headers/wasm/output_report.hpp b/headers/wasm/output_report.hpp
index 26bf54107..9eafa0eca 100644
--- a/headers/wasm/output_report.hpp
+++ b/headers/wasm/output_report.hpp
@@ -40,11 +40,11 @@ inline void dump_all_summary_json(const Profile_t &profile,
   ofs << "  \"not_to_explore_count\": " << overall.not_to_explore_count
       << ",\n";
   ofs << "  \"unreachable_count\": " << overall.unreachable_count;
-  if (PROFILE_STEP || PROFILE_TIME) {
+  if (PROFILE_STEP || PROFILE_TIME || PROFILE_SNAPSHOT) {
     ofs << ",\n";
     profile.write_as_json(ofs);
   }
   ofs << "}\n";
   ofs.close();
 }
-#endif // WASM_OUTPUT_REPORT_HPP
\ No newline at end of file
+#endif // WASM_OUTPUT_REPORT_HPP
diff --git a/headers/wasm/profile.hpp b/headers/wasm/profile.hpp
index 922b1d45f..fb0ab64ea 100644
--- a/headers/wasm/profile.hpp
+++ b/headers/wasm/profile.hpp
@@ -11,6 +11,7 @@
 #include <iomanip>
 #include <ratio>
 #include <string>
+#include <utility>
 #include <variant>
 #include <vector>
 
@@ -220,6 +221,11 @@ class Profile_t {
                        TimeProfileKind::COLLECT_PATH_CONDITIONS)]
                 << std::endl;
     }
+    if (PROFILE_SNAPSHOT) {
+      std::cout << "Snapshot Profile Summary:" << std::endl;
+      std::cout << "Total snapshot records: " << snapshot_history.size()
+                << std::endl;
+    }
     std::cout << "Number of calls to solver: " << call_solver_count
               << std::endl;
     std::cout << "Execution Kind Summary:" << std::endl;
@@ -235,72 +241,105 @@ class Profile_t {
 
   void write_as_json(std::ostream &os) const {
     os << "  \"profile_summary\": {\n";
+    bool needs_comma = false;
+    auto write_field_prefix = [&](const char *key) {
+      if (needs_comma) {
+        os << ",\n";
+      }
+      os << "    \"" << key << "\": ";
+      needs_comma = true;
+    };
+    auto write_field = [&](const char *key, const auto &value) {
+      write_field_prefix(key);
+      os << value;
+    };
     if (PROFILE_STEP) {
-      os << "    \"total_push_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::PUSH)] << ",\n";
-      os << "    \"total_pop_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::POP)] << ",\n";
-      os << "    \"total_peek_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::PEEK)] << ",\n";
-      os << "    \"total_shift_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::SHIFT)] << ",\n";
-      os << "    \"total_set_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::SET)] << ",\n";
-      os << "    \"total_get_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::GET)] << ",\n";
-      os << "    \"total_binary_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::BINARY)]
-         << ",\n";
-      os << "    \"total_tree_fill_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::TREE_FILL)]
-         << ",\n";
-      os << "    \"total_cursor_move_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::CURSOR_MOVE)]
-         << ",\n";
-      os << "    \"total_other_instructions_executed\": " << step_count
-         << ",\n";
-      os << "    \"total_mem_grow_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::MEM_GROW)]
-         << ",\n";
-      os << "    \"total_snapshot_create_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::SNAPSHOT_CREATE)]
-         << ",\n";
-      os << "    \"total_sym_eval_operations\": "
-         << op_count[static_cast<std::size_t>(StepProfileKind::SYM_EVAL)]
-         << "\n";
+      write_field(
+          "total_push_operations",
+          op_count[static_cast<std::size_t>(StepProfileKind::PUSH)]);
+      write_field("total_pop_operations",
+                  op_count[static_cast<std::size_t>(StepProfileKind::POP)]);
+      write_field("total_peek_operations",
+                  op_count[static_cast<std::size_t>(StepProfileKind::PEEK)]);
+      write_field("total_shift_operations",
+                  op_count[static_cast<std::size_t>(StepProfileKind::SHIFT)]);
+      write_field("total_set_operations",
+                  op_count[static_cast<std::size_t>(StepProfileKind::SET)]);
+      write_field("total_get_operations",
+                  op_count[static_cast<std::size_t>(StepProfileKind::GET)]);
+      write_field("total_binary_operations",
+                  op_count[static_cast<std::size_t>(StepProfileKind::BINARY)]);
+      write_field(
+          "total_tree_fill_operations",
+          op_count[static_cast<std::size_t>(StepProfileKind::TREE_FILL)]);
+      write_field(
+          "total_cursor_move_operations",
+          op_count[static_cast<std::size_t>(StepProfileKind::CURSOR_MOVE)]);
+      write_field("total_other_instructions_executed", step_count);
+      write_field("total_mem_grow_operations",
+                  op_count[static_cast<std::size_t>(StepProfileKind::MEM_GROW)]);
+      write_field("total_snapshot_create_operations",
+                  op_count[static_cast<std::size_t>(
+                      StepProfileKind::SNAPSHOT_CREATE)]);
+      write_field("total_sym_eval_operations",
+                  op_count[static_cast<std::size_t>(StepProfileKind::SYM_EVAL)]);
     }
     if (PROFILE_TIME) {
-      os << "    \"total_time_instruction_execution_s\": "
-         << std::setprecision(15)
-         << time_count[static_cast<std::size_t>(TimeProfileKind::INSTR)]
-         << ",\n";
-      os << "    \"total_time_solver_s\": " << std::setprecision(15)
+      write_field_prefix("total_time_instruction_execution_s");
+      os << std::setprecision(15)
+         << time_count[static_cast<std::size_t>(TimeProfileKind::INSTR)];
+      write_field_prefix("total_time_solver_s");
+      os << std::setprecision(15)
          << time_count[static_cast<std::size_t>(
-                TimeProfileKind::CALL_Z3_SOLVER)]
-         << ",\n";
-      os << "    \"total_time_resuming_from_snapshot_s\": "
-         << std::setprecision(15)
+                TimeProfileKind::SOLVER_TOTAL)];
+      write_field_prefix("total_time_z3_api_call_s");
+      os << std::setprecision(15)
          << time_count[static_cast<std::size_t>(
-                TimeProfileKind::RESUME_SNAPSHOT)]
-         << ",\n";
-      os << "    \"total_time_counting_symbolic_size_s\": "
-         << std::setprecision(15)
+                TimeProfileKind::CALL_Z3_SOLVER)];
+      write_field_prefix("total_time_resuming_from_snapshot_s");
+      os << std::setprecision(15)
          << time_count[static_cast<std::size_t>(
-                TimeProfileKind::COUNT_SYM_SIZE)]
-         << "\n";
-      os << "    \"total_time_splitting_path_conditions_s\": "
-         << std::setprecision(15)
+                TimeProfileKind::RESUME_SNAPSHOT)];
+      write_field_prefix("total_time_counting_symbolic_size_s");
+      os << std::setprecision(15)
          << time_count[static_cast<std::size_t>(
-                TimeProfileKind::SPLIT_CONDITIONS)]
-         << ",\n";
+                TimeProfileKind::COUNT_SYM_SIZE)];
+      write_field_prefix("total_time_splitting_path_conditions_s");
+      os << std::setprecision(15)
+         << time_count[static_cast<std::size_t>(
+                TimeProfileKind::SPLIT_CONDITIONS)];
+      write_field_prefix("total_time_main_loop_s");
+      os << std::setprecision(15)
+         << time_count[static_cast<std::size_t>(TimeProfileKind::MAIN_LOOP)];
     }
     if (PROFILE_CACHE) {
-      os << "    \"total_cache_hits\": " << cache_hit_count << ",\n";
-      os << "    \"total_cache_misses\": " << cache_miss_count << ",\n";
-      os << "    \"cache_hit_rate\": "
-         << static_cast<double>(cache_hit_count) /
-                static_cast<double>(cache_hit_count + cache_miss_count)
-         << "\n";
+      write_field("total_cache_hits", cache_hit_count);
+      write_field("total_cache_misses", cache_miss_count);
+      write_field("cache_hit_rate",
+                  static_cast<double>(cache_hit_count) /
+                      static_cast<double>(cache_hit_count + cache_miss_count));
+    }
+    if (PROFILE_SNAPSHOT) {
+      write_field("total_snapshot_records", snapshot_history.size());
+      write_field_prefix("snapshot_history");
+      os << "[";
+      for (std::size_t i = 0; i < snapshot_history.size(); ++i) {
+        if (i != 0) {
+          os << ",";
+        }
+        os << "\n      {"
+           << "\"resume_cost\": " << std::setprecision(15)
+           << snapshot_history[i].first << ", "
+           << "\"restart_cost\": " << std::setprecision(15)
+           << snapshot_history[i].second << "}";
+      }
+      if (!snapshot_history.empty()) {
+        os << "\n    ";
+      }
+      os << "]";
+    }
+    if (needs_comma) {
+      os << '\n';
     }
     os << "  }\n";
   }
@@ -338,6 +377,12 @@ class Profile_t {
     time_count[static_cast<std::size_t>(kind)] -= time;
   }
 
+  void record_snapshot_history(double resume_cost, double restart_cost) {
+    snapshot_history.emplace_back(resume_cost, restart_cost);
+  }
+
+  std::vector<std::pair<double, double>> snapshot_history;
+
   int step_count;
   std::array<int, static_cast<std::size_t>(StepProfileKind::OperationCount)>
       op_count;
@@ -413,4 +458,4 @@ struct CostManager_t {
 
 static CostManager_t CostManager;
 
-#endif // PROFILE_HPP
\ No newline at end of file
+#endif // PROFILE_HPP
diff --git a/headers/wasm/smt_solver.hpp b/headers/wasm/smt_solver.hpp
index 562eeecbf..08d3ea4c0 100644
--- a/headers/wasm/smt_solver.hpp
+++ b/headers/wasm/smt_solver.hpp
@@ -53,7 +53,8 @@ compose_query_results(const std::vector<QueryResult> &results) {
               starts_with(name, "s_f64")) &&
              "Unexpected declaration in query result model");
       assert(!combined_model.has_interp(decl) &&
-             "Internal Error: Conflicting constant declarations when composing query results");
+             "Internal Error: Conflicting constant declarations when composing "
+             "query results");
       z3::expr value = model.get_const_interp(decl);
       combined_model.add_const_interp(decl, value);
     }
@@ -450,8 +451,10 @@ inline std::monostate GENSYM_SYM_ASSERT(SymVal &sym_cond) {
   Profile.remove_instruction_time(TimeProfileKind::INSTR,
                                   time_need_to_be_removed.count());
   if (result.has_value()) {
-    std::cout << "Symbolic assertion failed" << std::endl;
-    throw std::runtime_error("Symbolic assertion failed");
+    GENSYM_INFO("Symbolic assertion failed");
+    if (!SOFT_ASSERT)
+      throw std::runtime_error("Symbolic assertion failed");
+    GENSYM_INFO("Soft assertion configured, continuing execution...");
   }
   return std::monostate{};
 }
diff --git a/headers/wasm/sym_rt.hpp b/headers/wasm/sym_rt.hpp
index 760112b5a..48ba32c75 100644
--- a/headers/wasm/sym_rt.hpp
+++ b/headers/wasm/sym_rt.hpp
@@ -425,7 +425,11 @@ class SymMemory_t {
     auto b1 = loadSymByte(base + offset + 1);
     auto b2 = loadSymByte(base + offset + 2);
     auto b3 = loadSymByte(base + offset + 3);
-    return SVFactory::make_smallbv(32, 0).concat(b3).concat(b2).concat(b1).concat(b0);
+    return SVFactory::make_smallbv(32, 0)
+        .concat(b3)
+        .concat(b2)
+        .concat(b1)
+        .concat(b0);
   }
 
   SymVal loadSymLong32S(int32_t base, int32_t offset) {
@@ -659,6 +663,15 @@ class SymEnv_t {
 
 static SymEnv_t SymEnv;
 
+inline Num isSymbolic(int index) {
+  auto it = SVFactory::SymbolStore.find(index);
+  if (it != SVFactory::SymbolStore.end()) {
+    return Num(I32V(1));
+  } else {
+    return Num(I32V(0));
+  }
+}
+
 // A snapshot of the symbolic state and execution context (control)
 class Snapshot_t {
 public:
@@ -732,9 +745,9 @@ struct NodeBox {
 
 struct Node {
   friend struct NodeBox;
-  virtual ~Node(){};
+  virtual ~Node() {};
   void set_cost(double c) { instr_cost = c; }
-  double get_cost() const { return instr_cost; }
+  double cost_of_restart() const { return instr_cost; }
   virtual std::string to_string() = 0;
   void to_graphviz(std::ostream &os) {
     os << "digraph G {\n";
@@ -775,7 +788,7 @@ struct Node {
 
 inline double NodeBox::instr_cost() const {
   if (node) {
-    return node->get_cost();
+    return node->cost_of_restart();
   } else {
     return 0.0;
   }
@@ -918,6 +931,8 @@ struct SnapshotNode : Node {
   const Snapshot_t &get_snapshot() const { return snapshot; }
   Snapshot_t move_out_snapshot() { return std::move(snapshot); }
 
+  double cost_of_snapshot_resume() const { return snapshot.cost_of_snapshot(); }
+
   bool worth_to_reuse() const {
     if (!ENABLE_COST_MODEL) {
       // If we are not using cost model, always create snapshot
@@ -925,7 +940,7 @@ struct SnapshotNode : Node {
     }
     // find out the best way to reach the current position via our cost model
     auto snapshot_cost = snapshot.cost_of_snapshot();
-    double re_execution_cost = get_cost();
+    double re_execution_cost = cost_of_restart();
     // std::cout << "Snapshot cost: " << snapshot_cost
     //           << ", re-execution cost: " << re_execution_cost << std::endl;
     if (snapshot_cost <= re_execution_cost) {
diff --git a/headers/wasm/symbolic_decl.hpp b/headers/wasm/symbolic_decl.hpp
index 0e2b5bd25..22bd4c03a 100644
--- a/headers/wasm/symbolic_decl.hpp
+++ b/headers/wasm/symbolic_decl.hpp
@@ -37,6 +37,7 @@ enum UnaryOperation {
   NOT,     // bool not
   BOOL2BV, // bool to bitvector,
   EXTEND,  // bitvector extension, extend i32 to i64
+  ABS,     // floating-point absolute value
 };
 
 enum ValueKind { KindBV, KindBool, KindFP };
@@ -110,7 +111,9 @@ struct SymExtract : public Symbolic {
   int low;
 
   SymExtract(SymVal value, int high, int low)
-      : value(value), high(high), low(low) {}
+      : value(value), high(high), low(low) {
+    assert(value->value_kind() == KindBV);
+  }
 
   int size() override {
     if (_cached_dag_size.has_value()) {
@@ -231,6 +234,10 @@ struct SymUnary : public Symbolic {
     case NOT:
       _width = 1;
       break;
+    case ABS:
+      assert(value->value_kind() == KindFP);
+      _width = value->width();
+      break;
     default:
       assert(false && "Unknown unary operation");
     }
@@ -254,6 +261,9 @@ struct SymUnary : public Symbolic {
     case BOOL2BV: {
       return ValueKind::KindBV;
     }
+    case ABS: {
+      return ValueKind::KindFP;
+    }
     default: {
       assert(false && "Unknown unary operation");
     }
diff --git a/headers/wasm/symbolic_impl.hpp b/headers/wasm/symbolic_impl.hpp
index 8c6fb067f..28e9795a3 100644
--- a/headers/wasm/symbolic_impl.hpp
+++ b/headers/wasm/symbolic_impl.hpp
@@ -155,6 +155,11 @@ inline z3::expr Symbolic::build_z3_expr_aux() {
       z3::expr bool_expr = unary->value->z3_expr();
       return z3::ite(bool_expr, one_bv, zero_bv);
     }
+    case ABS: {
+      z3::expr fp_expr = unary->value->z3_expr();
+      return z3::to_expr(global_z3_ctx(),
+                         Z3_mk_fpa_abs(global_z3_ctx(), fp_expr));
+    }
     default:
       throw std::runtime_error("Unary operation not supported: " +
                                std::to_string(unary->op));
diff --git a/headers/wasm/symval_decl.hpp b/headers/wasm/symval_decl.hpp
index 8f9ac1a30..b3739692b 100644
--- a/headers/wasm/symval_decl.hpp
+++ b/headers/wasm/symval_decl.hpp
@@ -51,6 +51,7 @@ struct SymVal {
   SymVal bitwise_and(const SymVal &other) const;
   SymVal bitwise_xor(const SymVal &other) const;
   SymVal bitwise_or(const SymVal &other) const;
+  SymVal abs() const;
   SymVal concat(const SymVal &other) const;
   SymVal extract(int high, int low) const;
   SymVal bv2bool() const;
@@ -84,6 +85,8 @@ template <typename... Args> inline bool allConcrete(const Args &...args) {
   return (... && args.is_concrete());
 }
 
+inline Num isSymbolic(int index);
+
 inline SymVal Concrete(Num num, int width);
 
 [[noreturn]] inline SymVal debug_unreachable(const char* msg) {
diff --git a/headers/wasm/symval_factory.hpp b/headers/wasm/symval_factory.hpp
index 14875764c..5c4a09a55 100644
--- a/headers/wasm/symval_factory.hpp
+++ b/headers/wasm/symval_factory.hpp
@@ -613,6 +613,22 @@ inline SymVal make_unary(UnaryOperation op, const SymVal &value) {
     }
   }
 
+  if (op == ABS) {
+    if (auto concrete = dynamic_cast<SymConcrete *>(value.symptr.get())) {
+      if (concrete->kind == KindFP) {
+        if (concrete->width() == 32) {
+          auto result = SVFactory::make_concrete_fp(concrete->value.f32_abs(), 32);
+          UnaryOperationStore.insert({key, result});
+          return result;
+        } else if (concrete->width() == 64) {
+          auto result = SVFactory::make_concrete_fp(concrete->value.f64_abs(), 64);
+          UnaryOperationStore.insert({key, result});
+          return result;
+        }
+      }
+    }
+  }
+
   auto result = SymVal(SVFactory::SymBookKeeper.allocate<SymUnary>(op, value));
   UnaryOperationStore.insert({key, result});
   return result;
diff --git a/headers/wasm/symval_impl.hpp b/headers/wasm/symval_impl.hpp
index b7b3684c9..d05d30cae 100644
--- a/headers/wasm/symval_impl.hpp
+++ b/headers/wasm/symval_impl.hpp
@@ -125,6 +125,10 @@ inline SymVal SymVal::bool_not() const {
   return SVFactory::make_unary(NOT, *this);
 }
 
+inline SymVal SymVal::abs() const {
+  return SVFactory::make_unary(ABS, *this);
+}
+
 inline SymVal SymVal::concat(const SymVal &other) const {
   return SVFactory::make_concat(*this, other);
 }
diff --git a/headers/wasm/utils.hpp b/headers/wasm/utils.hpp
index 62c5bb8a2..2782d6d90 100644
--- a/headers/wasm/utils.hpp
+++ b/headers/wasm/utils.hpp
@@ -1,15 +1,24 @@
 #ifndef UTILS_HPP
 #define UTILS_HPP
+#include "config.hpp"
+#include <cstddef>
+#include <cstdint>
 #include <iostream>
+#include <limits>
+#include <unordered_map>
 #include <variant>
 
 #ifndef GENSYM_ASSERT
 #define GENSYM_ASSERT(condition)                                               \
   do {                                                                         \
     if (!(condition)) {                                                        \
-      throw std::runtime_error(std::string("Assertion failed: ") + " (" +      \
-                               __FILE__ + ":" + std::to_string(__LINE__) +     \
-                               ")");                                           \
+      std::string message = std::string("Assertion failed: ") + " (" +         \
+                            __FILE__ + ":" + std::to_string(__LINE__) + ")";   \
+      if (SOFT_ASSERT) {                                                       \
+        GENSYM_INFO(message);                                                  \
+      } else {                                                                 \
+        throw std::runtime_error(message);                                     \
+      }                                                                        \
     }                                                                          \
   } while (0)
 #endif
@@ -38,6 +47,68 @@
 
 #endif
 
+enum class GensymHeapStatus { Allocated, Freed };
+
+struct GensymHeapRecord {
+  int32_t size;
+  GensymHeapStatus status;
+};
+
+inline std::unordered_map<int32_t, GensymHeapRecord> GENSYM_HEAP_RECORDS;
+
+inline bool GENSYM_IS_IN_ALLOCATED_RANGE(int32_t addr, size_t width) {
+  const int64_t start = addr;
+  const int64_t end = start + static_cast<int64_t>(width);
+  for (const auto &[base, record] : GENSYM_HEAP_RECORDS) {
+    if (record.status != GensymHeapStatus::Allocated) {
+      continue;
+    }
+    const int64_t alloc_start = base;
+    const int64_t alloc_end = alloc_start + static_cast<int64_t>(record.size);
+    if (alloc_start <= start && end <= alloc_end) {
+      return true;
+    }
+  }
+  return false;
+}
+
+inline bool GENSYM_SHOULD_CHECK_ALLOCATION(int32_t addr) {
+  if (GENSYM_HEAP_RECORDS.empty()) {
+    return false;
+  }
+  int32_t heap_base = std::numeric_limits<int32_t>::max();
+  for (const auto &[base, _] : GENSYM_HEAP_RECORDS) {
+    heap_base = std::min(heap_base, base);
+  }
+  return addr >= heap_base;
+}
+
+inline void GENSYM_ASSERT_ADDR_ALLOCATED(int32_t addr, size_t width) {
+  if (!GENSYM_SHOULD_CHECK_ALLOCATION(addr)) {
+    return;
+  }
+  GENSYM_ASSERT(GENSYM_IS_IN_ALLOCATED_RANGE(addr, width));
+}
+
+inline int32_t GENSYM_ALLOC(int32_t base, int32_t size) {
+  // std::cout << "Allocating memory at address " << base << " with size " << size
+  //           << std::endl;
+  GENSYM_ASSERT(base >= 0);
+  GENSYM_ASSERT(size >= 0);
+  GENSYM_HEAP_RECORDS[base] =
+      GensymHeapRecord{size, GensymHeapStatus::Allocated};
+  return base;
+}
+
+inline std::monostate GENSYM_FREE(int32_t ptr) {
+  // std::cout << "Freeing memory at address " << ptr << std::endl;
+  GENSYM_ASSERT(ptr >= 0);
+  auto it = GENSYM_HEAP_RECORDS.find(ptr);
+  GENSYM_ASSERT(it != GENSYM_HEAP_RECORDS.end());
+  it->second.status = GensymHeapStatus::Freed;
+  return std::monostate{};
+}
+
 #if __cplusplus < 202002L
 #include <string>
 
@@ -89,4 +160,4 @@ std::monostate infoWhen(const char *dbg_option, const Args &...args) {
 inline std::monostate get_unit() { return std::monostate{}; }
 inline std::monostate get_unit(std::monostate x) { return std::monostate{}; }
 
-#endif // UTILS_HPP
\ No newline at end of file
+#endif // UTILS_HPP
diff --git a/scripts/genwasym_profile_analyzer.py b/scripts/genwasym_profile_analyzer.py
new file mode 100755
index 000000000..b9313a7df
--- /dev/null
+++ b/scripts/genwasym_profile_analyzer.py
@@ -0,0 +1,111 @@
+#!/usr/bin/env python3
+
+import argparse
+import csv
+import json
+import sys
+from pathlib import Path
+from typing import Any
+
+
+def parse_args() -> argparse.Namespace:
+    parser = argparse.ArgumentParser(
+        description="Analyze a GenWasm profile JSON file."
+    )
+    parser.add_argument("profile", type=Path, help="profile JSON file to read")
+    parser.add_argument(
+        "-o",
+        "--output",
+        type=Path,
+        help="CSV file to write; defaults to stdout",
+    )
+    parser.add_argument(
+        "--plot",
+        type=Path,
+        help="write a snapshot cost scatter plot to this image file",
+    )
+    return parser.parse_args()
+
+
+def snapshot_costs(profile: dict[str, Any]) -> tuple[list[float], list[float]]:
+    history = profile.get("profile_summary", {}).get("snapshot_history", [])
+    restart_costs = []
+    resume_costs = []
+    for entry in history:
+        restart_costs.append(float(entry["restart_cost"]))
+        resume_costs.append(float(entry["resume_cost"]))
+    return restart_costs, resume_costs
+
+
+def write_snapshot_csv(profile: dict[str, Any], output_file: Any) -> None:
+    restart_costs, resume_costs = snapshot_costs(profile)
+    writer = csv.writer(output_file)
+    writer.writerow(["restart_cost", "resume_cost"])
+    writer.writerows(zip(restart_costs, resume_costs))
+
+
+def write_snapshot_plot(profile: dict[str, Any], output: Path) -> None:
+    try:
+        import matplotlib
+
+        matplotlib.use("Agg")
+        import matplotlib.pyplot as plt
+    except ImportError as exc:
+        raise RuntimeError(
+            "plotting requires matplotlib; install it with "
+            "`python3 -m pip install matplotlib`"
+        ) from exc
+
+    restart_costs, resume_costs = snapshot_costs(profile)
+    if not restart_costs:
+        raise ValueError("profile does not contain snapshot history records")
+
+    min_restart_cost = min(restart_costs)
+    max_restart_cost = max(restart_costs)
+    x_margin = (max_restart_cost - min_restart_cost) * 0.05
+    if x_margin == 0:
+        x_margin = max_restart_cost * 0.05
+    x_min = min_restart_cost - x_margin
+    x_max = max_restart_cost + x_margin
+
+    y_min = 0
+    y_max = max(resume_costs) * 1.05
+    line_max = min(x_max, y_max)
+    line_min = max(x_min, y_min)
+
+    fig, ax = plt.subplots(figsize=(8, 6))
+    ax.scatter(restart_costs, resume_costs, s=14, alpha=0.75)
+    ax.plot([line_min, line_max], [line_min, line_max], color="black", linewidth=1.2)
+    ax.set_xlabel("restart_cost")
+    ax.set_ylabel("resume_cost")
+    ax.set_title("Snapshot cost profile")
+    ax.set_xlim(x_min, x_max)
+    ax.set_ylim(y_min, y_max)
+    ax.grid(True, linewidth=0.4, alpha=0.4)
+    fig.tight_layout()
+    fig.savefig(output)
+    plt.close(fig)
+
+
+def main() -> None:
+    args = parse_args()
+    with args.profile.open() as profile_file:
+        profile = json.load(profile_file)
+
+    output_file = args.output.open("w", newline="") if args.output else sys.stdout
+    try:
+        write_snapshot_csv(profile, output_file)
+    finally:
+        if args.output:
+            output_file.close()
+
+    if args.plot:
+        try:
+            write_snapshot_plot(profile, args.plot)
+        except RuntimeError as exc:
+            print(f"error: {exc}", file=sys.stderr)
+            raise SystemExit(1) from exc
+
+
+if __name__ == "__main__":
+    main()
diff --git a/src/main/scala/wasm/Parser.scala b/src/main/scala/wasm/Parser.scala
index 4841261f8..9206451c8 100644
--- a/src/main/scala/wasm/Parser.scala
+++ b/src/main/scala/wasm/Parser.scala
@@ -491,6 +491,7 @@ class GSWasmVisitor extends WatParserBaseVisitor[WIR] {
         case "reinterpret" =>
           val fromTy = toNumType(fromTySign)
           Reinterpret(fromTy, toTy)
+        case _ => throw new RuntimeException(s"Unsupported convert opcode: ${ctx.CONVERT.getText}")
       }
       Convert(op)
     } else if (ctx.SYM_ASSERT != null) {
diff --git a/src/main/scala/wasm/StagedConcolicMiniWasm.scala b/src/main/scala/wasm/StagedConcolicMiniWasm.scala
index fa441d5cc..82faf70eb 100644
--- a/src/main/scala/wasm/StagedConcolicMiniWasm.scala
+++ b/src/main/scala/wasm/StagedConcolicMiniWasm.scala
@@ -515,6 +515,11 @@ trait ConcreteOps extends StagedWasmValueDomains with ValueCreation {
       }
     }
 
+    def abs(): StagedConcreteNum = num.tipe match {
+      case NumType(F32Type) => StagedConcreteNum(NumType(F32Type), "f32-unary-abs".reflectCtrlWith[Num](num.i))
+      case NumType(F64Type) => StagedConcreteNum(NumType(F64Type), "f64-unary-abs".reflectCtrlWith[Num](num.i))
+    }
+
     def extendS(): StagedConcreteNum = num.tipe match {
       case NumType(I32Type) => StagedConcreteNum(NumType(I64Type), "i32-extend-to-i64-s".reflectCtrlWith[Num](num.i))
     }
@@ -559,6 +564,14 @@ trait ConcreteOps extends StagedWasmValueDomains with ValueCreation {
       case NumType(F64Type) => StagedConcreteNum(NumType(I32Type), "f64-trunc-to-i32-u".reflectCtrlWith[Num](num.i))
     }
 
+    def truncF32ToI32S(): StagedConcreteNum = num.tipe match {
+      case NumType(F32Type) => StagedConcreteNum(NumType(I32Type), "f32-trunc-to-i32-s".reflectCtrlWith[Num](num.i))
+    }
+
+    def truncF32ToI32U(): StagedConcreteNum = num.tipe match {
+      case NumType(F32Type) => StagedConcreteNum(NumType(I32Type), "f32-trunc-to-i32-u".reflectCtrlWith[Num](num.i))
+    }
+
     def assert(): Rep[Unit] = {
       "assert-true".reflectCtrlWith[Unit](num.toInt != 0)
     }
@@ -596,6 +609,11 @@ trait SymbolicOps extends StagedWasmValueDomains {
       case NumType(I64Type) => StagedSymbolicNum(NumType(I64Type), "sym-popcnt".reflectCtrlWith[SymVal](num.s))
     }
 
+    def abs(): StagedSymbolicNum = num.tipe match {
+      case NumType(F32Type) => StagedSymbolicNum(NumType(F32Type), "sym-unary-abs".reflectCtrlWith[SymVal](num.s))
+      case NumType(F64Type) => StagedSymbolicNum(NumType(F64Type), "sym-unary-abs".reflectCtrlWith[SymVal](num.s))
+    }
+
     def +(rhs: StagedSymbolicNum): StagedSymbolicNum = {
       (num.tipe, rhs.tipe) match {
         case (NumType(I32Type), NumType(I32Type)) =>
@@ -1612,7 +1630,12 @@ trait StagedWasmEvaluator extends SAIOps
           val newRestCtx = restCtx.shift(offset, funcTy.out.size)
           eval(rest, kont, trail)(newRestCtx)
         })
-        eval(inner, restK _, restK _ :: trail)
+        def innerK: Rep[Cont[Unit]] = topFun((_: Rep[Unit]) => {
+          info(s"Entering the block, stackSize =", Stack.size)
+          eval(inner, restK _, restK _ :: trail)
+        })
+        tailCall(innerK, ())
+        ()
       case Loop(ty, inner) =>
         val funcTy = ty.funcType
         val exitSize = ctx.stackTypes.size - funcTy.inps.size + funcTy.out.size
@@ -1920,23 +1943,37 @@ trait StagedWasmEvaluator extends SAIOps
           v.assert()
         }
         eval(rest, kont, trail)(newCtx)
+      case Import("i32", "is_symbolic", _) =>
+        val newCtx2 = withBlock {
+          val (ty, newCtx) = ctx.pop()
+          Stack.popC(ty)
+          Stack.popS(ty)
+          val (ty1, newCtx1) = ctx.pop()
+          val idx = Stack.popC(ty1)
+          Stack.popS(ty)
+          Stack.pushC(isSymbolic(idx.toInt))
+          newCtx1.push(NumType(I32Type))
+        }
+        eval(rest, kont, trail)(newCtx2)
       case Import("mem", "alloc", _) =>
         // this semantics here is not standardized in wasp, here is wasp's impl
         // https://github.com/formalsec/wasp/blob/release/0.2.3/wasp/symbolic/concolic.ml#L449
         val (_, newCtx1) = ctx.pop()
-        val a = Stack.popC(NumType(I32Type))
+        val size = Stack.popC(NumType(I32Type))
         Stack.popS(NumType(I32Type))
         val (_, newCtx2) = newCtx1.pop()
-        val b = Stack.popC(NumType(I32Type))
+        val base = Stack.popC(NumType(I32Type))
         Stack.popS(NumType(I32Type))
-        Stack.pushC(b)
-        val s = "Concrete".reflectCtrlWith[SymVal](Values.I32V(b.toInt), 32)
+        val ptr = Values.I32V(gensymAlloc(base.toInt, size.toInt))
+        Stack.pushC(StagedConcreteNum(NumType(I32Type), ptr))
+        val s = "Concrete".reflectCtrlWith[SymVal](ptr, 32)
         Stack.pushS(StagedSymbolicNum(NumType(I32Type), s))
         eval(rest, kont, trail)(newCtx1)
       case Import("mem", "free", _) =>
         val (_, newCtx) = ctx.pop()
-        Stack.popC(NumType(I32Type))
+        val ptr = Stack.popC(NumType(I32Type))
         Stack.popS(NumType(I32Type))
+        gensymFree(ptr.toInt)
         eval(rest, kont, trail)(newCtx)
       case Import("env", "proc_exit", _) =>
         val (_, newCtx) = ctx.pop()
@@ -1961,7 +1998,8 @@ trait StagedWasmEvaluator extends SAIOps
     case Clz(_) => value.clz()
     case Ctz(_) => value.ctz()
     case Popcnt(_) => value.popcnt()
-    case _ => ???
+    case Abs(_) => value.abs()
+    case _ => throw new Exception(s"Unknown unary operation $op")
   }
 
   def evalUnaryOpS(op: UnaryOp, value: StagedSymbolicNum, c: StagedConcreteNum): StagedSymbolicNum = {
@@ -1972,6 +2010,7 @@ trait StagedWasmEvaluator extends SAIOps
         case Clz(_)   => value.clz()
         case Ctz(_)   => value.ctz()
         case Popcnt(_) => value.popcnt()
+        case Abs(_)   => value.abs()
         case _        => throw new Exception(s"Unknown unary operation $op")
       }).s
     }
@@ -2080,6 +2119,8 @@ trait StagedWasmEvaluator extends SAIOps
     case ConvertTo(NumType(I32Type), NumType(F64Type), ZX) => value.convertI32ToF64U()
     case ConvertTo(NumType(I64Type), NumType(F64Type), SX) => value.convertI64ToF64S()
     case ConvertTo(NumType(I64Type), NumType(F64Type), ZX) => value.convertI64ToF64U()
+    case TruncTo(NumType(F32Type), NumType(I32Type), SX) => value.truncF32ToI32S()
+    case TruncTo(NumType(F32Type), NumType(I32Type), ZX) => value.truncF32ToI32U()
     case TruncTo(NumType(F64Type),NumType(I32Type),ZX) => value.truncF64ToI32U()
     case _ => throw new UnsupportedOperationException(s"Unsupported concrete conversion $op")
   }
@@ -2160,6 +2201,18 @@ trait StagedWasmEvaluator extends SAIOps
     "reset-stacks".reflectCtrlWith[Unit]()
   }
 
+  def gensymAlloc(base: Rep[Int], size: Rep[Int]): Rep[Int] = {
+    "gensym-alloc".reflectCtrlWith[Int](base, size)
+  }
+
+  def gensymFree(ptr: Rep[Int]): Rep[Unit] = {
+    "gensym-free".reflectCtrlWith[Unit](ptr)
+  }
+
+  def isSymbolic(index: Rep[Int]): StagedConcreteNum = {
+    StagedConcreteNum(NumType(I32Type), "is-symbolic".reflectCtrlWith[Num](index))
+  }
+
   def evalSeq(instrs: List[Instr],
               kont: Context => Rep[Cont[Unit]],
               trail: Trail[Unit]): Rep[Unit] = {
@@ -2208,7 +2261,7 @@ trait StagedWasmEvaluator extends SAIOps
             evalSeq(offset, (_: Context) => forwardKont, ((_: Context) => forwardKont)::Nil)
             val offsetC = Stack.popC(NumType(I32Type))
             Stack.popS(NumType(I32Type))
-            Predef.println(s"funcIndices: $funcIndices")
+            // Predef.println(s"funcIndices: $funcIndices")
             for ((fidx, i) <- funcIndices.asInstanceOf[ElemListFunc].funcs.view.zipWithIndex) {
               val FuncDef(_, FuncBodyDef(ty, _, bodyLocals, body)) = module.funcs(fidx)
               val func = evalFunc(ty, body, fidx, ty.inps, bodyLocals)
@@ -2495,6 +2548,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
       emit("(0 == "); shallow(num); emit(")")
     case Node(_, "sym-is-zero", List(s_num), _) =>
       shallow(s_num); emit(".is_zero().bool2bv()")
+    case Node(_, "sym-unary-abs", List(s_num), _) =>
+      shallow(s_num); emit(".abs()")
     case Node(_, "i32-binary-add", List(lhs, rhs), _) =>
       shallow(lhs); emit(".i32_add("); shallow(rhs); emit(")")
     case Node(_, "i64-binary-add", List(lhs, rhs), _) =>
@@ -2605,8 +2660,16 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
       emit("("); shallow(num); emit(".convert_i64_to_f64_s())")
     case Node(_, "i64-convert-to-f64-u", List(num), _) =>
       emit("("); shallow(num); emit(".convert_i64_to_f64_u())")
+    case Node(_, "f32-trunc-to-i32-s", List(num), _) =>
+      emit("("); shallow(num); emit(".trunc_f32_to_i32_s())")
+    case Node(_, "f32-trunc-to-i32-u", List(num), _) =>
+      emit("("); shallow(num); emit(".trunc_f32_to_i32_u())")
     case Node(_, "f64-trunc-to-i32-u", List(num), _) =>
       emit("("); shallow(num); emit(".trunc_f64_to_i32_u())")
+    case Node(_, "f32-unary-abs", List(num), _) =>
+      emit("("); shallow(num); emit(".f32_abs())")
+    case Node(_, "f64-unary-abs", List(num), _) =>
+      emit("("); shallow(num); emit(".f64_abs())")
     case Node(_, "f32-binary-add", List(lhs, rhs), _) =>
       shallow(lhs); emit(".f32_add("); shallow(rhs); emit(")")
     case Node(_, "f64-binary-add", List(lhs, rhs), _) =>
@@ -2695,6 +2758,10 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
       shallow(lhs); emit(".rem_u("); shallow(rhs); emit(")")
     case Node(_, "sym-i32-extend-to-i64", List(num), _) =>
       shallow(num); emit(".extend_to_i64()")
+    case Node(_, "gensym-alloc", List(base, size), _) =>
+      emit("GENSYM_ALLOC("); shallow(base); emit(", "); shallow(size); emit(")")
+    case Node(_, "gensym-free", List(ptr), _) =>
+      emit("GENSYM_FREE("); shallow(ptr); emit(")")
     case Node(_, "num-to-int", List(num), _) =>
       shallow(num); emit(".toInt()")
     case Node(_, "make-i32-symbol", List(num), _) =>
@@ -2739,6 +2806,8 @@ trait StagedWasmCppGen extends CGenBase with CppSAICodeGenBase {
       emit("prependCont(");  shallow(kont); emit(", "); shallow(mkont); emit(")")
     case Node(_, "enter-current-mkont", List(), _) =>
       emit("enterCC(std::monostate())")
+    case Node(_, "is-symbolic", List(index), _) =>
+      emit("isSymbolic("); shallow(index); emit(")")
     case Node(_, "init-func-table", List(offset, i, func), _) =>
       emit("FuncTable.set("); shallow(offset); emit(", "); shallow(i); emit(", "); shallow(func); emit(")")
     case Node(_, "tree-fill-call-indirect", List(s, id), _) =>
diff --git a/src/test/scala/genwasym/TestBenchmark.scala b/src/test/scala/genwasym/TestBenchmark.scala
index ab962f61c..ee88e7287 100644
--- a/src/test/scala/genwasym/TestBenchmark.scala
+++ b/src/test/scala/genwasym/TestBenchmark.scala
@@ -37,12 +37,31 @@ class TestBenchmark extends FunSuite {
     }
   }
 
-  test("compile-btree-benchmarks") { compileDirToCpp("./benchmarks/pldi2026/btree/", Some("main")) }
+  def compileDirTreeToCpp(dir: String,
+                          main: Option[String] = None): Unit = {
+    import java.io.File
+
+    def walk(file: File): Unit = {
+      if (file.isDirectory) {
+        Option(file.listFiles()).getOrElse(Array.empty).foreach(walk)
+      } else if (file.getName.endsWith(".wat")) {
+        compileToCpp(file.getAbsolutePath, main)
+      }
+    }
+
+    walk(new File(dir))
+  }
+
+  test("compile-btree-benchmarks") { compileDirToCpp("./benchmarks/pldi2026/btree/tests-normalized", Some("main")) }
   test("compile-crafted-benchmarks") { compileDirToCpp("./benchmarks/pldi2026/crafted/") }
   test("compile-aws-aws-encryption-sdk") { compileDirToCpp("./benchmarks/pldi2026/aws-encryption-sdk/tests-original-normalized/", Some("__original_main")) }
+  test("compile-collection-c-benchmarks") { compileDirTreeToCpp("./benchmarks/pldi2026/Collection-C/tests-normalized/", Some("__original_main")) }
+  test("compile-quicksort-benchmark") { compileDirToCpp("/home/zdh/WorkSpace/cJSON", Some("main")) }
   test("compile-a-single-file") {
     sys.env.get("INPUT") match {
-      case Some(path) => compileToCpp(path)
+      case Some(path) =>
+        val main = sys.env.get("MAIN")
+        compileToCpp(path, main)
       case None => println("Environment variable INPUT not set; skipping compileToCpp")
     }
   }
diff --git a/src/test/scala/genwasym/TestStagedConcolicEval.scala b/src/test/scala/genwasym/TestStagedConcolicEval.scala
index 4df5b0122..21535d9be 100644
--- a/src/test/scala/genwasym/TestStagedConcolicEval.scala
+++ b/src/test/scala/genwasym/TestStagedConcolicEval.scala
@@ -207,7 +207,11 @@ class TestStagedConcolicEval extends CppCompilationTestBase {
   }
 
   test("call-indirect-concrete") {
-    testFileConcreteCpp("./benchmarks/wasm/call_indirect_test.wat", expect=Some(List(42)))
+    testFileConcreteCpp("./benchmarks/wasm/call_indirect_test.wat", expect=Some(List(38)))
+  }
+
+  test("call-indirect-offset-concrete") {
+    testFileConcreteCpp("./benchmarks/wasm/call_indirect_test.1.wat", expect=Some(List(38)))
   }
 
   test("data-section-concrete") {