Return vacuous on undefined concrete terms

runtimeverification · Aug 21, 2024 · df4cfae · df4cfae
1 parent 39e6abc
commit df4cfae
Showing 1 changed file with 11 additions and 6 deletions.
diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
@@ -162,15 +162,20 @@ respond stateVar request =
                                 checkConstraintsConsistent
                                 substPat
 
+                        let trivialResponse =
+                                execResponse
+                                    req
+                                    (0, mempty, RewriteTrivial substPat)
+                                    substitution
+                                    unsupported
+
                         case evaluatedInitialPattern of
                             (Left ApplyEquations.SideConditionFalse{}, _) -> do
                                 -- input pattern's constraints are Bottom, return Vacuous
-                                pure $
-                                    execResponse
-                                        req
-                                        (0, mempty, RewriteTrivial substPat)
-                                        substitution
-                                        unsupported
+                                pure trivialResponse
+                            (Left ApplyEquations.UndefinedTerm{}, _) -> do
+                                -- LLVM has stumbled upon an undefined term, the whole term is Bottom, return Vacuous
+                                pure trivialResponse
                             (Left other, _) ->
                                 pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
                             (Right newPattern, simplifierCache) -> do