Merge remote-tracking branch 'upstream/develop' into cvc5-set-bag

ucsd-progsys · Feb 6, 2025 · ba83438 · ba83438
2 parents 89677fb + 32e943d
commit ba83438
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 5 deletions.
diff --git a/liquid-fixpoint b/liquid-fixpoint
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Generate.hs
@@ -280,11 +280,10 @@ killSubst :: RReft -> RReft
 killSubst = fmap killSubstReft
 
 killSubstReft :: F.Reft -> F.Reft
-killSubstReft = trans kv () ()
+killSubstReft = trans ks
   where
-    kv    = defaultVisitor { txExpr = ks }
-    ks _ (F.PKVar k _) = F.PKVar k mempty
-    ks _ p             = p
+    ks (F.PKVar k _) = F.PKVar k mempty
+    ks p             = p
 
 defAnn :: Bool -> t -> Annot t
 defAnn True  = AnnRDf
+2 −0		liquid-fixpoint.cabal
+11 −11		src/Language/Fixpoint/Horn/Transformations.hs
+0 −12		src/Language/Fixpoint/Solver/Sanitize.hs
+148 −127		src/Language/Fixpoint/SortCheck.hs
+249 −92		src/Language/Fixpoint/Types/Visitor.hs