Skip to content

Commit

Permalink
Throw an exception when no candidates for an uninterpreted name are f…
Browse files Browse the repository at this point in the history
…ound (#1673)

* Throw an exception when no uninterpreted names are found

* Add an integration test
  • Loading branch information
chameco authored Jun 1, 2022
1 parent af9172f commit baa55df
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 3 deletions.
1 change: 1 addition & 0 deletions intTests/test_resolve_unint_missing/test.saw
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
fails (prove_print (w4_unint_yices ["foo"]) {{ True }});
4 changes: 4 additions & 0 deletions intTests/test_resolve_unint_missing/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
#!/bin/sh
set -e

$SAW test.saw
8 changes: 5 additions & 3 deletions src/SAWScript/Builtins.hs
Original file line number Diff line number Diff line change
Expand Up @@ -515,12 +515,14 @@ resolveName sc nm =
do resolvedName <- io $ scResolveNameByURI sc uri
case resolvedName of
Just vi -> pure $ vi:scnms
Nothing -> pure scnms
_ -> pure scnms
Nothing -> pure scnms
Nothing -> fallback scnms
_ -> fallback scnms
Nothing -> fallback scnms

where
tnm = Text.pack nm
fallback [] = fail $ "Could not resolve name: " <> show nm
fallback scnms = pure scnms


normalize_term :: TypedTerm -> TopLevel TypedTerm
Expand Down

0 comments on commit baa55df

Please sign in to comment.