Skip to content

Commit

Permalink
Add case for DeltaSat results from SBV.
Browse files Browse the repository at this point in the history
  • Loading branch information
robdockins committed Sep 8, 2021
1 parent cedfd0d commit 5056038
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions src/SAWScript/Prover/SBV.hs
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,8 @@ proveUnintSBVIO sc conf unintSet timeout goal =
r' = SBVSim.getLabels labels dict argNames
return (r', stats)

SBV.DeltaSat{} -> fail "Prover returned an unexpected DeltaSat result"

SBV.SatExtField {} -> fail "Prover returned model in extension field"

SBV.Unknown {} -> fail "Prover returned Unknown"
Expand Down

0 comments on commit 5056038

Please sign in to comment.