From 8596907aeafae0ebd3a53e7a2b335d0b99aa9d59 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Fri, 30 Apr 2021 12:24:21 -0700
Subject: [PATCH] Make `goal_eval_unint` work with polymorphic functions.

Fixes #1045.
---
 saw-core-what4/src/Verifier/SAW/Simulator/What4.hs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
index 05d1495748..be2114cd59 100644
--- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
+++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -1359,6 +1359,10 @@ mkArgTerm sc ty val =
          x <- scCtorApp sc i xs
          return (ArgTermConst x)
 
+    (_, TValue tval) ->
+      do x <- termOfTValue sc tval
+         pure (ArgTermConst x)
+
     _ -> fail $ "could not create uninterpreted function argument of type " ++ show ty
 
 termOfTValue :: SharedContext -> TValue (What4 sym) -> IO Term