diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.cs | 9 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 2 |
2 files changed, 6 insertions, 5 deletions
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 9b7b6e36..bb225071 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -100,8 +100,9 @@ namespace Microsoft.Boogie { /// <summary>
/// Constructor. Initialize a checker with the program and log file.
+ /// Optionally, use prover context provided by parameter "ctx".
/// </summary>
- public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout) {
+ public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, int timeout, ProverContext ctx = null) {
Contract.Requires(vcgen != null);
Contract.Requires(prog != null);
this.timeout = timeout;
@@ -121,7 +122,6 @@ namespace Microsoft.Boogie { options.Parse(CommandLineOptions.Clo.ProverOptions);
ContextCacheKey key = new ContextCacheKey(prog);
- ProverContext ctx;
ProverInterface prover;
if (vcgen.CheckerCommonState == null) {
@@ -129,12 +129,13 @@ namespace Microsoft.Boogie { }
IDictionary<ContextCacheKey, ProverContext>/*!>!*/ cachedContexts = (IDictionary<ContextCacheKey, ProverContext/*!*/>)vcgen.CheckerCommonState;
- if (cachedContexts.TryGetValue(key, out ctx)) {
+ if (ctx == null && cachedContexts.TryGetValue(key, out ctx))
+ {
ctx = (ProverContext)cce.NonNull(ctx).Clone();
prover = (ProverInterface)
CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx);
} else {
- ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
+ if (ctx == null) ctx = (ProverContext)CommandLineOptions.Clo.TheProverFactory.NewProverContext(options);
// set up the context
foreach (Declaration decl in prog.TopLevelDeclarations) {
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index d13811e0..db7f2dca 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2454,7 +2454,7 @@ namespace VC {
GenerateVCForStratifiedInlining(program, info, checker);
}
- //Console.WriteLine("Inlining {0}", procName);
+ Console.WriteLine("Inlining {0}", procName);
VCExpr expansion = cce.NonNull(info.vcexpr);
// Instantiate the "forall" variables
|