diff options
| author |  qadeer <unknown> | 2010-02-16 23:04:53 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-02-16 23:04:53 +0000 |
| commit | 0549304b5beaf553ba3e5fa6550a6b8e43e31553 (patch) | |
| tree | 1333dc7fd6b911b4a2e0cd001c7dd3955e1c5c40 /Source/Provers/Z3 | |
| parent | 717eaee0063074b804098d3cfd44a7a3f822b064 (diff) | |
1. Removed a quadratic loop in SimplifyLikeLineariser.ssc in favor of a linear procedure call
2. Inlining requires two fields OriginalBlocks and OriginalLocVars in Implementation. These are set just before inlining is called and now I reset them to null afterwards to help garbage collection.
3. Clear live variables right after passification again to help garbage collection.
Diffstat (limited to 'Source/Provers/Z3')
| -rw-r--r-- | Source/Provers/Z3/ProverInterface.ssc | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Source/Provers/Z3/ProverInterface.ssc b/Source/Provers/Z3/ProverInterface.ssc index c3a61fe3..9a28eb42 100644 --- a/Source/Provers/Z3/ProverInterface.ssc +++ b/Source/Provers/Z3/ProverInterface.ssc @@ -169,6 +169,13 @@ namespace Microsoft.Boogie.Z3 allVars.Add(furtherVar);
return new Z3LineariserOptions(AsTerm, opts, allVars);
}
+
+ public override LineariserOptions! AddLetVariables(List<VCExprVar!>! furtherVars) {
+ List<VCExprVar!>! allVars = new List<VCExprVar!> ();
+ allVars.AddRange(LetVariables);
+ allVars.AddRange(furtherVars);
+ return new Z3LineariserOptions(AsTerm, opts, allVars);
+ }
}
// -----------------------------------------------------------------------------------------------
|