summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-04-26 12:57:16 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-04-26 12:59:56 +0100
commitbed8d4a027c635a146911a2ce973046f02a8e719 (patch)
tree7a9727ea29cbcfebe8786db31ee499e0620e044d /Test
parent9af64efeb4a057f853bb08cfc0fa8cbdc4a166b2 (diff)
Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a
variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error
Diffstat (limited to 'Test')
-rw-r--r--Test/prover/usedot.bpl9
1 files changed, 9 insertions, 0 deletions
diff --git a/Test/prover/usedot.bpl b/Test/prover/usedot.bpl
new file mode 100644
index 00000000..5815236e
--- /dev/null
+++ b/Test/prover/usedot.bpl
@@ -0,0 +1,9 @@
+// RUN: %boogie -typeEncoding:m -proverLog:"%t.smt2" "%s"
+// RUN: %OutputCheck "%s" --file-to-check="%t.smt2"
+procedure foo() {
+ // . is an illegal starting character in SMT-LIBv2
+ // so test that we don't emit it as a symbol name.
+ // CHECK-L:(declare-fun q@.x () Int)
+ var .x:int;
+ assert .x == 0;
+}