Skip to content

Commit 0d99509

Browse files
author
Brian Huffman
committed
Make goal_eval_unint handle functions with arguments of type Nat.
We can now make functions like `take` and `drop` uninterpreted. Fixes #1588.
1 parent 64abd30 commit 0d99509

File tree

1 file changed

+4
-0
lines changed
  • saw-core-what4/src/Verifier/SAW/Simulator

1 file changed

+4
-0
lines changed

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

+4
Original file line numberDiff line numberDiff line change
@@ -1519,6 +1519,10 @@ mkArgTerm sc ty val =
15191519
do x <- termOfTValue sc tval
15201520
pure (ArgTermConst x)
15211521

1522+
(_, VNat n) ->
1523+
do x <- scNat sc n
1524+
pure (ArgTermConst x)
1525+
15221526
_ -> fail $ "could not create uninterpreted function argument of type " ++ show ty
15231527

15241528
termOfTValue :: SharedContext -> TValue (What4 sym) -> IO Term

0 commit comments

Comments
 (0)