implemented /UseUnsatCoreForInlining option for use in stratified inlining

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs
index 2f2f03ce..5f776bff 100644
--- a/Source/Provers/Z3api/ProverLayer.cs
+++ b/Source/Provers/Z3api/ProverLayer.cs
@@ -99,11 +99,11 @@ namespace Microsoft.Boogie.Z3
             outcome = cm.Check(out z3LabelModels);

         }

 

-        public override void CheckAssumptions(List<VCExpr> assumptions)

+        public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)

         {

             Z3SafeContext cm = context.cm;

             LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());

-            outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels);

+            outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);

         }

 

         public override void Push()