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] 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