Use substitution in Implies

runtimeverification · Oct 22, 2024 · b2ea0f8 · b2ea0f8
1 parent bc72188
commit b2ea0f8
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 4 deletions.
diff --git a/booster/library/Booster/Pattern/Implies.hs b/booster/library/Booster/Pattern/Implies.hs
@@ -122,7 +122,7 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                         , substitution = substitutionR
                                         }
 
-                            SMT.isSat solver (Set.toList substPatL.constraints) >>= \case
+                            SMT.isSat solver (Set.toList substPatL.constraints) substPatL.substitution >>= \case
                                 SMT.IsUnsat ->
                                     let sort = externaliseSort $ sortOfPattern substPatL
                                      in implies' (Kore.Syntax.KJBottom sort) sort antecedent.term consequent.term mempty
@@ -159,8 +159,10 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
                                     pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)
                         MatchSuccess subst -> do
                             let filteredConsequentPreds =
-                                    Set.map (Substitution.substituteInPredicate subst) substPatR.constraints
-                                        `Set.difference` substPatL.constraints
+                                    Set.map
+                                        (Substitution.substituteInPredicate subst)
+                                        (substPatR.constraints <> (Set.fromList $ Substitution.asEquations substPatR.substitution))
+                                        `Set.difference` (substPatL.constraints <> (Set.fromList $ Substitution.asEquations substPatL.substitution))
 
                             if null filteredConsequentPreds
                                 then

diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs
@@ -280,8 +280,9 @@ isSat ::
     Log.LoggerMIO io =>
     SMT.SMTContext ->
     [Predicate] ->
+    Map Variable Term -> -- supplied substitution
     io (IsSatResult ())
-isSat ctxt ps = fmap void <$> (isSatReturnTransState ctxt ps mempty)
+isSat ctxt ps subst = fmap void <$> (isSatReturnTransState ctxt ps subst)
 
 {- |
 Implementation of get-model request