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

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;
+}