Skip to content

Commit 748c998

Browse files
committed
Include input substitution into the pattern
1 parent c527a80 commit 748c998

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

booster/library/Booster/JsonRpc.hs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,7 @@ respond stateVar request =
137137
{ term = substituteInTerm substitution term
138138
, constraints = Set.fromList $ map (substituteInPredicate substitution) preds
139139
, ceilConditions = ceils
140-
, substitution = mempty -- this is the ensures-substitution, leave empty
140+
, substitution
141141
}
142142
-- remember all variables used in the substitutions
143143
substVars =
@@ -255,7 +255,7 @@ respond stateVar request =
255255
{ term = substituteInTerm substitution pat.term
256256
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
257257
, ceilConditions = pat.ceilConditions
258-
, substitution = mempty -- this is the ensures-substitution, leave empty
258+
, substitution
259259
}
260260
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty substPat >>= \case
261261
(Right newPattern, _) -> do
@@ -290,7 +290,7 @@ respond stateVar request =
290290
mLlvmLibrary
291291
solver
292292
mempty
293-
predicates
293+
predicates -- TODO include ps.substitution?
294294
>>= \case
295295
(Right newPreds, _) -> do
296296
let predicateSort =

0 commit comments

Comments
 (0)