From 3cf6e54ed70626614e4db2fb731918bc8b060f87 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Sun, 17 Jan 2021 12:04:19 -0800
Subject: [PATCH 1/2] Make `goal_eval` preserve pi-bound variables in goals.

Fixes #985.
---
 src/SAWScript/Builtins.hs | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index f249d1e6d3..57b6972925 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -536,13 +536,23 @@ goal_eval unints =
   withFirstGoal $ \goal ->
   do sc <- getSharedContext
      unintSet <- resolveNames unints
-     t0 <- liftIO $ propToPredicate sc (goalProp goal)
+     -- replace all pi-bound quantified variables with new free variables
+     let (args, body) = asPiList (unProp (goalProp goal))
+     body' <-
+       case asEqTrue body of
+         Just t -> pure t
+         Nothing -> fail "goal_eval: expected EqTrue"
+     ecs <- liftIO $ traverse (\(nm, ty) -> scFreshEC sc (Text.unpack nm) ty) args
+     vars <- liftIO $ traverse (scExtCns sc) ecs
+     t0 <- liftIO $ instantiateVarList sc 0 (reverse vars) body'
      let gen = globalNonceGenerator
      sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen
      (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym sc Map.empty unintSet t0
      t1 <- liftIO $ Crucible.toSC sym p
      t2 <- liftIO $ scEqTrue sc t1
-     return ((), mempty, Just (goal { goalProp = Prop t2 }))
+     -- turn the free variables we generated back into pi-bound variables
+     t3 <- liftIO $ scGeneralizeExts sc ecs t2
+     return ((), mempty, Just (goal { goalProp = Prop t3 }))
 
 beta_reduce_goal :: ProofScript ()
 beta_reduce_goal =

From 0f045d2627bb52c1f057afdfd5deaa30e8f98c26 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 22 Jan 2021 04:27:12 -0800
Subject: [PATCH 2/2] Add regression test for issue #985.

---
 intTests/test_goal_eval/test.saw | 25 +++++++++++++++++++++++++
 intTests/test_goal_eval/test.sh  |  1 +
 2 files changed, 26 insertions(+)
 create mode 100644 intTests/test_goal_eval/test.saw
 create mode 100644 intTests/test_goal_eval/test.sh

diff --git a/intTests/test_goal_eval/test.saw b/intTests/test_goal_eval/test.saw
new file mode 100644
index 0000000000..96cf9f552e
--- /dev/null
+++ b/intTests/test_goal_eval/test.saw
@@ -0,0 +1,25 @@
+// This is a regression test for GaloisInc/saw-script#985.
+// It uses `goal_eval` and then calls `goal_intro` to enforce
+// that `goal_eval` has preserved the explicit quantifiers in
+// the goal.
+
+enable_experimental;
+
+let prop = {{ \(xs:[4][8]) (ys:([8],[8])) -> sum xs == ys.0 * ys.1 }};
+
+prove
+  do {
+    goal_intro "z";
+    assume_unsat;
+  }
+  prop;
+
+prove
+  do {
+    goal_eval;
+    goal_intro "z";
+    assume_unsat;
+  }
+  prop;
+
+print "Done";
diff --git a/intTests/test_goal_eval/test.sh b/intTests/test_goal_eval/test.sh
new file mode 100644
index 0000000000..0b864017cd
--- /dev/null
+++ b/intTests/test_goal_eval/test.sh
@@ -0,0 +1 @@
+$SAW test.saw