Merge pull request #1283 from GaloisInc/issue1045

Make `goal_eval_unint` work with polymorphic functions.
GaloisInc · May 5, 2021 · 6d3f39c · 6d3f39c
2 parents c1851b2 + a24bb18
commit 6d3f39c
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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