Make goal_eval_unint handle functions with arguments of type Nat.

We can now make functions like `take` and `drop` uninterpreted. Fixes #1588.
GaloisInc · Feb 21, 2022 · 147209b · 147209b
1 parent a134e4a
commit 147209b
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
@@ -1519,6 +1519,10 @@ mkArgTerm sc ty val =
       do x <- termOfTValue sc tval
          pure (ArgTermConst x)
 
+    (_, VNat n) ->
+      do x <- scNat sc n
+         pure (ArgTermConst x)
+
     _ -> fail $ "could not create uninterpreted function argument of type " ++ show ty
 
 termOfTValue :: SharedContext -> TValue (What4 sym) -> IO Term