summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/VC.cs
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2014-06-28 15:54:30 +0530
committerGravatar akashlal <unknown>2014-06-28 15:54:30 +0530
commitb3c1b63ae910ec9df00594d7d14e852cf7e709e5 (patch)
tree7a16dd97df45da5f5f7ce291658c8f2eafeed545 /Source/VCGeneration/VC.cs
parentc87e9aa5300dde782b7d0a0069ac7ddbc14e6697 (diff)
OnModel now carries the result of the prover call
Diffstat (limited to 'Source/VCGeneration/VC.cs')
-rw-r--r--Source/VCGeneration/VC.cs4
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 53868e1d..bfff8f0e 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1881,7 +1881,7 @@ namespace VC {
this.program = program;
}
- public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) {
//Contract.Requires(cce.NonNullElements(labels));
if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
if (VC.ConditionGeneration.errorModelList != null)
@@ -1970,7 +1970,7 @@ namespace VC {
Contract.Requires(program != null);
}
- public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model, ProverInterface.Outcome proverOutcome) {
//Contract.Requires(cce.NonNullElements(labels));
// We ignore the error model here for enhanced error message purposes.
// It is only printed to the command line.