Panic if we depend on a theorem that hasn't been registered in the da…

…tabase.
GaloisInc · May 21, 2021 · 0e496b0 · 0e496b0
1 parent cbc7727
commit 0e496b0
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
@@ -309,8 +309,8 @@ reachableTheorems db roots =
             (Map.insert curr thm visited)
             (thmDepends thm)
 
-     | otherwise = visited -- TODO? maybe panic here?
-
+     | otherwise =
+         panic "reachableTheorems" ["Could not find theorem with identifier", show (indexValue curr)]
 
 -- | Check that the purported theorem is valid.
 --