diff options
| author |  tabarbe <unknown> | 2010-07-22 20:56:13 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-07-22 20:56:13 +0000 |
| commit | 589fb634c9cff46508bdf5c1ef2929524fdc8f6a (patch) | |
| tree | a18cb1345b461d51bbc8f63c61397c8ad7e0f9bf /Source/Provers/Z3/ProverInterface.cs | |
| parent | 11e5d0540d8f787beba021a67514a463459ea464 (diff) | |
Boogie: Repaired a reentrancy error in Z3/Simplify.
Diffstat (limited to 'Source/Provers/Z3/ProverInterface.cs')
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.cs | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs index 824dabd4..994cb282 100644 --- a/Source/Provers/Z3/ProverInterface.cs +++ b/Source/Provers/Z3/ProverInterface.cs @@ -65,10 +65,11 @@ void ObjectInvariant() return new Z3ProverProcess(opts, inspector);
}
- protected override AxiomVCExprTranslator SpawnVCExprTranslator() {
+ protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) {
+ Contract.Requires(opts != null);
Contract.Ensures(Contract.Result<AxiomVCExprTranslator>() != null);
- return new Z3VCExprTranslator(gen, opts);
+ return new Z3VCExprTranslator(gen, (Z3InstanceOptions) opts);
}
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
|