Skip to content

Commit c4325bb

Browse files
committed
Remove Kore.Internal.SideCondition.assertNormalized
The normalization check doesn't seem to serve any purpose: it is regularly violated, and the only thing we can do with the SideCondition is send it to the solver, which doesn't care about our definition of normalization.
1 parent 81d7006 commit c4325bb

File tree

1 file changed

+4
-13
lines changed

1 file changed

+4
-13
lines changed

kore/src/Kore/Internal/SideCondition.hs

Lines changed: 4 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -152,12 +152,11 @@ andCondition
152152
-> Condition variable
153153
-> SideCondition variable
154154
andCondition SideCondition { assumedTrue } newCondition =
155-
assertNormalized result result
155+
SideCondition
156+
{ representation = toRepresentationCondition merged
157+
, assumedTrue = merged
158+
}
156159
where
157-
result = SideCondition
158-
{ representation = toRepresentationCondition merged
159-
, assumedTrue = merged
160-
}
161160
merged = assumedTrue `Condition.andCondition` newCondition
162161

163162
assumeTrueCondition
@@ -209,11 +208,3 @@ toRepresentationCondition =
209208

210209
isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool
211210
isNormalized = Conditional.isNormalized . from @_ @(Condition variable)
212-
213-
assertNormalized
214-
:: forall variable a
215-
. HasCallStack
216-
=> Ord variable
217-
=> SideCondition variable
218-
-> a -> a
219-
assertNormalized = Conditional.assertNormalized . from @_ @(Condition variable)

0 commit comments

Comments
 (0)