diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt index 06a41cf3496..671f606aef8 100644 --- a/regression/cbmc-incr-smt2/CMakeLists.txt +++ b/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" + "$ --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" + "$ --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" + "-C;-s;new-smt-z3" + "CORE" + ) -add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests} -) + add_test_pl_profile( + "cbmc-new-smt-backend-cvc5" + "$ --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" + "-C;-s;new-smt-cvc5" + "CORE" + ) +endif() diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile index 603200de746..8697b4d8eee 100644 --- a/regression/cbmc-incr-smt2/Makefile +++ b/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 diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc index 4e2f90d69b1..d45e6ebe787 100644 --- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc +++ b/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 diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc index 6149a33f6d1..55f19120fb0 100644 --- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc +++ b/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\) diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc index 8ae4bae24b7..499ccbe044b 100644 --- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc +++ b/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 diff --git a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc b/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc index db0157d613b..52ecdacce30 100644 --- a/regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc +++ b/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 diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc index e5431ba76e6..44db46465de 100644 --- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc +++ b/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 diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc index e6248c053ea..ffe947dd21e 100644 --- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc +++ b/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$ diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc index d7e290ae8b8..4d9dee8aabd 100644 --- a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc +++ b/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$ diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc index 9f093877f9f..0279e9b9725 100644 --- a/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc +++ b/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 diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc index 9c561b2433b..8b3cce08da5 100644 --- a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc +++ b/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$ diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc index cb971aec828..83540d3754d 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc +++ b/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 diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc index 38b41075e78..95eb34be616 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc +++ b/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 diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc index 2135ea76791..61d49d1fbe5 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc +++ b/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\) diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc index d7546c34f8c..69bdd2bf605 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc +++ b/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 diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc index e34ae2426b4..7535bf54fa0 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc +++ b/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 diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp index 8a7c8cc70c1..81bcfe908d6 100644 --- a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp +++ b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp @@ -13,12 +13,191 @@ #include #include +#include #include #include #include +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) + "|"; } diff --git a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp index 4f1475e922f..2ce204b28c6 100644 --- a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp +++ b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp @@ -11,9 +11,29 @@ #include #include +#include + TEST_CASE("Test smt_indext to string conversion", "[core][smt2_incremental]") { - CHECK(smt_to_smt2_string(smt_symbol_indext{"green"}) == "|green|"); + std::string input_term; + std::string expected_term; + using rowt = std::pair; + + std::tie(input_term, expected_term) = GENERATE( + rowt{"green", "green"}, + rowt{"abc76473*^&", "abc76473*^&"}, + rowt{"my name is", "|my name is|"}, + // The following are example symbols from the SMTLIB spec. + rowt{"+", "+"}, + rowt{"**", "**"}, + rowt{".kkk", ".kkk"}, + rowt{"-32", "-32"}, + rowt{" \" can occur too", "| \" can occur too|"}); + + SECTION("check that index identifiers are constructed accordingly") + { + CHECK(smt_to_smt2_string(smt_symbol_indext{input_term}) == expected_term); + } CHECK(smt_to_smt2_string(smt_numeral_indext{42}) == "42"); } @@ -36,7 +56,7 @@ TEST_CASE( { CHECK( smt_to_smt2_string(smt_bit_vector_theoryt::extract(7, 3)( - smt_bit_vector_constant_termt{0, 8})) == "((_ |extract| 7 3) (_ bv0 8))"); + smt_bit_vector_constant_termt{0, 8})) == "((_ extract 7 3) (_ bv0 8))"); } TEST_CASE( @@ -51,15 +71,30 @@ TEST_CASE( "Test smt_identifier_termt to string conversion", "[core][smt2_incremental]") { + std::string input_term; + std::string expected_term; + using rowt = std::pair; + + std::tie(input_term, expected_term) = GENERATE( + rowt{"abc", "abc"}, + rowt{"\\", "|&92;|"}, + rowt{"green", "green"}, + rowt{"abc76473*^&", "abc76473*^&"}, + rowt{"my name is", "|my name is|"}, + // The following are example symbols from the SMTLIB spec. + rowt{"+", "+"}, + rowt{"**", "**"}, + rowt{".kkk", ".kkk"}, + rowt{"-32", "-32"}, + rowt{" \" can occur too", "| \" can occur too|"}); + SECTION("Simple identifiers") { CHECK( - smt_to_smt2_string(smt_identifier_termt{"abc", smt_bool_sortt{}}) == - "|abc|"); - CHECK( - smt_to_smt2_string(smt_identifier_termt{"\\", smt_bool_sortt{}}) == - "|&92;|"); + smt_to_smt2_string(smt_identifier_termt{input_term, smt_bool_sortt{}}) == + expected_term); } + SECTION("Indexed identifier") { CHECK( @@ -67,7 +102,7 @@ TEST_CASE( "foo", smt_bool_sortt{}, {smt_symbol_indext{"bar"}, smt_numeral_indext{42}}}) == - "(_ |foo| |bar| 42)"); + "(_ foo bar 42)"); } } @@ -78,8 +113,7 @@ TEST_CASE( CHECK( smt_to_smt2_string(smt_core_theoryt::equal( smt_identifier_termt{"foo", smt_bit_vector_sortt{32}}, - smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})) == - "(|=| |foo| |bar|)"); + smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})) == "(= foo bar)"); } TEST_CASE( @@ -102,7 +136,7 @@ TEST_CASE( { CHECK( smt_to_smt2_string(smt_get_value_commandt{ - smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value (|foo|))"); + smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value (foo))"); } TEST_CASE( @@ -138,7 +172,7 @@ TEST_CASE( smt_to_smt2_string(smt_declare_function_commandt{ smt_identifier_termt{"f", smt_bit_vector_sortt{31}}, {smt_bit_vector_sortt{32}, smt_bit_vector_sortt{33}}}) == - "(declare-fun |f| ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))"); + "(declare-fun f ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))"); } TEST_CASE( @@ -151,8 +185,7 @@ TEST_CASE( CHECK( smt_to_smt2_string(smt_define_function_commandt{ "f", {g, h}, smt_core_theoryt::equal(g, h)}) == - "(define-fun |f| ((|g| (_ BitVec 32)) (|h| (_ BitVec 32))) Bool (|=| |g| " - "|h|))"); + "(define-fun f ((g (_ BitVec 32)) (h (_ BitVec 32))) Bool (= g h))"); } TEST_CASE(