Add case for DeltaSat results from SBV.

GaloisInc · Aug 25, 2021 · 455c4ba · 455c4ba
1 parent 22c4584
commit 455c4ba
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/SAWScript/Prover/SBV.hs b/src/SAWScript/Prover/SBV.hs
@@ -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"