diff options
author | qadeer <unknown> | 2011-02-06 06:13:47 +0000 |
---|---|---|
committer | qadeer <unknown> | 2011-02-06 06:13:47 +0000 |
commit | 3718f4836a0a5d80b07f2e9f41cacbebbf7958fe (patch) | |
tree | 75799a4a9330f355e58f66a612e0cc7de646a769 /Source/Provers/Z3api/ProverLayer.cs | |
parent | 0f96c5cb02b4f1354841f22d29a7dbc86a12be51 (diff) |
implemented /UseUnsatCoreForInlining option for use in stratified inlining
Diffstat (limited to 'Source/Provers/Z3api/ProverLayer.cs')
-rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 4 |
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()
|