summaryrefslogtreecommitdiff
path: root/Source/Core/VCExp.cs
diff options
context:
space:
mode:
authorGravatar Peter Collingbourne <peter@pcc.me.uk>2012-09-06 20:33:21 +0100
committerGravatar Peter Collingbourne <peter@pcc.me.uk>2012-09-06 20:33:21 +0100
commit85a65323bda16d372a9e163dc4225e5d5535d14c (patch)
tree6e4999e040de5a5c7511521939c576957509b538 /Source/Core/VCExp.cs
parentf369261b5b9953380d8fb8e0f7b020167482a491 (diff)
Implement support for alternative SMT solvers -- CVC3 and CVC4
Diffstat (limited to 'Source/Core/VCExp.cs')
-rw-r--r--Source/Core/VCExp.cs4
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 6bc43e14..1e82224c 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -202,6 +202,10 @@ The generic options may or may not be used by the prover plugin.
}
}
+ public virtual bool SupportsLabels(ProverOptions options) {
+ return true;
+ }
+
public virtual void Close() {
}