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