From 52f94d26e9d66693e28fa7489368b5ee350accec Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 4 Oct 2024 13:32:13 +0200
Subject: [PATCH] Resetting heap instead of throwing away entire state after
 checking assertion

---
 src/main/scala/rules/Evaluator.scala | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala
index 11046c651..b0d116432 100644
--- a/src/main/scala/rules/Evaluator.scala
+++ b/src/main/scala/rules/Evaluator.scala
@@ -1030,8 +1030,9 @@ object evaluator extends EvaluationRules {
           => Q(s4, r4._1, r4._2, v4))
 
       case ast.Asserting(eAss, eIn) =>
-        consume(s, eAss, pve, v)((_, _, _) => {
-          eval(s, eIn, pve, v)(Q)
+        consume(s, eAss, pve, v)((s2, _, v2) => {
+          val s3 = s2.copy(g = s.g, h = s.h)
+          eval(s3, eIn, pve, v2)(Q)
         })
 
       /* Sequences */