Allow unquoted symbols in new SMT backend output if they observe the simple_symbols definition.

regression/cbmc-incr-smt2/CMakeLists.txt

@@ -1,10 +1,24 @@
-
+# On Windows, run only z3 tests
 if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-    set(exclude_win_broken_tests -X winbug)
+    add_test_pl_profile(
+        "cbmc-new-smt-backend-z3"
+        "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula"
+        "-C;X;winbug;-s;new-smt-z3"
+        "CORE"
+    )
 else()
-    set(exclude_win_broken_tests "")
-endif()
+    # On Unix systems, run both z3 and cvc5
+    add_test_pl_profile(
+        "cbmc-new-smt-backend-z3"
+        "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula"
+        "-C;-s;new-smt-z3"
+        "CORE"
+    )
 
-add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests}
-)
+    add_test_pl_profile(
+        "cbmc-new-smt-backend-cvc5"
+        "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula"
+        "-C;-s;new-smt-cvc5"
+        "CORE"
+    )
+endif()

regression/cbmc-incr-smt2/Makefile

@@ -9,8 +9,13 @@ else
 	exclude_broken_windows_tests=
 endif
 
-test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
+test: ../test.pl test.z3
+
+test.z3:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
+
+test.cvc5:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang smt --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
 
 tests.log: ../test.pl test
 

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc

@@ -1,6 +1,6 @@
 CORE
 overflow_behaviour.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ Wrap-around to INT_MIN when adding to INT_MAX: SUCCESS
 \[main\.assertion\.2\] line \d+ Wrap-around to INT_MAX when subtracting from INT_MIN: SUCCESS
 \[main\.assertion\.3\] line \d+ INT_MAX minus INT_MIN equals -1: SUCCESS

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc

@@ -1,6 +1,6 @@
 CORE
 polynomial.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ No negative solution: FAILURE
 \[main\.assertion\.2\] line \d+ No positive solution: FAILURE
 x=-8\ \(11111111 11111111 11111111 11111000\)

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc

@@ -1,6 +1,6 @@
 CORE
 simple_equation.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace --verbosity 10
+--trace --verbosity 10
 \[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS
 \[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS
 \[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc

@@ -1,6 +1,6 @@
 CORE
 unsigned_behaviour.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ a plus b should be more than 27: FAILURE
 \[main\.assertion\.2\] line \d+ a plus b should be more than 27: FAILURE
 \[main\.assertion\.3\] line \d+ c plus d should be more than 27: FAILURE

regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc

@@ -1,6 +1,6 @@
 CORE
 bitwise_ops.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+--slice-formula
 \[main\.assertion\.1\] line \d+ This is going to fail for bit-opposites: FAILURE
 \[main\.assertion\.2\] line \d+ This is going to hold for all values != 0: SUCCESS
 \[main\.assertion\.3\] line \d+ This is going to fail for the same value in A and B: FAILURE

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc

@@ -1,6 +1,6 @@
 CORE
 shift_left.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+--slice-formula
 \[main\.assertion\.1\] line \d Shifted result should be greater than one: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc

@@ -1,10 +1,10 @@
 CORE
 shift_right.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --trace
+--slice-formula --trace
 \[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE
 \[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
 \[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS
-second=128
+second=[128|\d+]
 result_unsigned=64
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc

@@ -1,6 +1,6 @@
 CORE
 div_by_zero.c
---incremental-smt2-solver 'z3 --smt2 -in' --div-by-zero-check --trace
+--div-by-zero-check --trace
 \[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE
 \[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS
 y=0

regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc

@@ -1,6 +1,6 @@
 CORE
 signed_overflow.c
---incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace
+--signed-overflow-check --trace
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc

@@ -1,22 +1,22 @@
 CORE
 control_flow.c
---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--verbosity 10
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)
 Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\)
 Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool |goto_symex::&92;guard#1|\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(assert \(|=| |goto_symex::&92;guard#1| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+Sending command to SMT2 solver - \(assert \(= |goto_symex::&92;guard#1| \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
 Sending command to SMT2 solver - \(declare-fun |main::1::y!0@1#4| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(assert \(|=| |main::1::y!0@1#4| \(|ite| |goto_symex::&92;guard#1| \(_ bv9 32\) \(_ bv4 32\)\)\)\)
+Sending command to SMT2 solver - \(assert \(= |main::1::y!0@1#4| \(|ite| |goto_symex::&92;guard#1| \(_ bv9 32\) \(_ bv4 32\)\)\)\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#3| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(assert \(|=| |main::1::x!0@1#3| \(|ite| |goto_symex::&92;guard#1| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)
+Sending command to SMT2 solver - \(assert \(= |main::1::x!0@1#3| \(|ite| |goto_symex::&92;guard#1| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)
 Sending command to SMT2 solver - \(declare-fun |main::1::z!0@1#2| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(assert \(|=| |main::1::z!0@1#2| |main::1::y!0@1#4|\)\)
-Sending command to SMT2 solver - \(define-fun |B3| \(\) Bool \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)
-Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#3| |main::1::z!0@1#2|\)\)\)\)
-Sending command to SMT2 solver - \(define-fun |B4| \(\) Bool \(|not| false\)\)
+Sending command to SMT2 solver - \(assert \(= |main::1::z!0@1#2| |main::1::y!0@1#4|\)\)
+Sending command to SMT2 solver - \(define-fun |B3| \(\) Bool \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)
+Sending command to SMT2 solver - \(assert \(not \(not \(= |main::1::x!0@1#3| |main::1::z!0@1#2|\)\)\)\)
+Sending command to SMT2 solver - \(define-fun |B4| \(\) Bool \(not false\)\)
 Sending command to SMT2 solver - \(assert |B4|\)
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - sat

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -1,14 +1,14 @@
 CORE
 test.c
---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--verbosity 10
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)
 Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
-Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
-Sending command to SMT2 solver - \(define-fun |B2| \(\) Bool \(|not| false\)\)
+Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+Sending command to SMT2 solver - \(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+Sending command to SMT2 solver - \(define-fun |B2| \(\) Bool \(not false\)\)
 Sending command to SMT2 solver - \(assert |B2|\)
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - sat

regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc

@@ -1,7 +1,7 @@
 CORE
 stdbool_example.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--trace
+Passing problem to incremental SMT2 solving via
 VERIFICATION FAILED
 equal=FALSE\s*\([0 ]+\)
 equal=TRUE\s*\([0 ]+1\)

regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc

@@ -1,7 +1,7 @@
 CORE
 trace.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--trace
+Passing problem to incremental SMT2 solving via
 Assert of inequality to 4\.: FAILURE
 Assert of inequality to 2\.: FAILURE
 y=4

regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc

@@ -1,7 +1,7 @@
 CORE
 valid_unsat.c
---incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+--verbosity 10
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - unsat
 VERIFICATION SUCCESSFUL

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -13,12 +13,191 @@
 
 #include <functional>
 #include <iostream>
+#include <regex>
 #include <sstream>
 #include <stack>
 #include <string>
 
+static bool is_simple_identifier(const std::string &identifier)
+{
+  PRECONDITION(!identifier.empty());
+  auto iterator = identifier.begin();
+  switch(*iterator)
+  {
+    case 'A':
+    case 'a':
+    case 'B':
+    case 'b':
+    case 'C':
+    case 'c':
+    case 'D':
+    case 'd':
+    case 'E':
+    case 'e':
+    case 'F':
+    case 'f':
+    case 'G':
+    case 'g':
+    case 'H':
+    case 'h':
+    case 'I':
+    case 'i':
+    case 'J':
+    case 'j':
+    case 'K':
+    case 'k':
+    case 'L':
+    case 'l':
+    case 'M':
+    case 'm':
+    case 'N':
+    case 'n':
+    case 'O':
+    case 'o':
+    case 'P':
+    case 'p':
+    case 'Q':
+    case 'q':
+    case 'R':
+    case 'r':
+    case 'S':
+    case 's':
+    case 'T':
+    case 't':
+    case 'U':
+    case 'u':
+    case 'V':
+    case 'v':
+    case 'W':
+    case 'w':
+    case 'X':
+    case 'x':
+    case 'Y':
+    case 'y':
+    case 'Z':
+    case 'z':
+    case '~':
+    case '!':
+    case '@':
+    case '$':
+    case '%':
+    case '^':
+    case '&':
+    case '*':
+    case '_':
+    case '-':
+    case '+':
+    case '=':
+    case '<':
+    case '>':
+    case '.':
+    case '?':
+    case '/':
+      ++iterator;
+      for(; iterator != identifier.cend(); ++iterator)
+      {
+        switch(*iterator)
+        {
+          case 'A':
+          case 'a':
+          case 'B':
+          case 'b':
+          case 'C':
+          case 'c':
+          case 'D':
+          case 'd':
+          case 'E':
+          case 'e':
+          case 'F':
+          case 'f':
+          case 'G':
+          case 'g':
+          case 'H':
+          case 'h':
+          case 'I':
+          case 'i':
+          case 'J':
+          case 'j':
+          case 'K':
+          case 'k':
+          case 'L':
+          case 'l':
+          case 'M':
+          case 'm':
+          case 'N':
+          case 'n':
+          case 'O':
+          case 'o':
+          case 'P':
+          case 'p':
+          case 'Q':
+          case 'q':
+          case 'R':
+          case 'r':
+          case 'S':
+          case 's':
+          case 'T':
+          case 't':
+          case 'U':
+          case 'u':
+          case 'V':
+          case 'v':
+          case 'W':
+          case 'w':
+          case 'X':
+          case 'x':
+          case 'Y':
+          case 'y':
+          case 'Z':
+          case 'z':
+          case '~':
+          case '!':
+          case '@':
+          case '$':
+          case '%':
+          case '^':
+          case '&':
+          case '*':
+          case '_':
+          case '-':
+          case '+':
+          case '=':
+          case '<':
+          case '>':
+          case '.':
+          case '?':
+          case '/':
+          case '0':
+          case '1':
+          case '2':
+          case '3':
+          case '4':
+          case '5':
+          case '6':
+          case '7':
+          case '8':
+          case '9':
+            continue;
+            // ok;
+          default:
+            return false;
+        }
+      }
+      break;
+    default:
+      return false;
+  }
+  return true;
+}
+
 static std::string escape_identifier(const irep_idt &identifier)
 {
+  // This matches the definition of a `simple_symbol` according to the SMTLIB
+  // specification, version 2.6.
+  const auto &id_string = id2string(identifier);
+  if(is_simple_identifier(id_string))
+    return id_string;
+
   return std::string{"|"} + smt2_convt::convert_identifier(identifier) + "|";
 }