Include substitution when checking LHS for SAT in Implies

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

Hide file tree

Showing 2 changed files with 3 additions and 2 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

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