summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
diff options
context:
space:
mode:
authorGravatar akashlal <unknown>2014-09-24 15:04:51 +0530
committerGravatar akashlal <unknown>2014-09-24 15:04:51 +0530
commitd335ace6437fb1639bea6f425811b9b54936d141 (patch)
treec50542be538a793d6912a351fbb84f3f8b07c78c /Source/Provers/SMTLib/ProverInterface.cs
parent716dc807128ac5bed97b22af0144ef516a3721e5 (diff)
Simple VC generation for SI
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs5
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 6b8e03d1..a94983e2 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -1248,7 +1248,10 @@ namespace Microsoft.Boogie.SMTLib
xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();
}
}
- else {
+ else if(CommandLineOptions.Clo.SIBoolControlVC) {
+ labels = new string[0];
+ xlabels = labels;
+ } else {
labels = CalculatePath(handler.StartingProcId());
xlabels = labels;
}