Skip to content

Commit df4cfae

Browse files
committed
Return vacuous on undefined concrete terms
1 parent 39e6abc commit df4cfae

File tree

1 file changed

+11
-6
lines changed

1 file changed

+11
-6
lines changed

booster/library/Booster/JsonRpc.hs

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -162,15 +162,20 @@ respond stateVar request =
162162
checkConstraintsConsistent
163163
substPat
164164

165+
let trivialResponse =
166+
execResponse
167+
req
168+
(0, mempty, RewriteTrivial substPat)
169+
substitution
170+
unsupported
171+
165172
case evaluatedInitialPattern of
166173
(Left ApplyEquations.SideConditionFalse{}, _) -> do
167174
-- input pattern's constraints are Bottom, return Vacuous
168-
pure $
169-
execResponse
170-
req
171-
(0, mempty, RewriteTrivial substPat)
172-
substitution
173-
unsupported
175+
pure trivialResponse
176+
(Left ApplyEquations.UndefinedTerm{}, _) -> do
177+
-- LLVM has stumbled upon an undefined term, the whole term is Bottom, return Vacuous
178+
pure trivialResponse
174179
(Left other, _) ->
175180
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
176181
(Right newPattern, simplifierCache) -> do

0 commit comments

Comments
 (0)