diff --git a/regression/cbmc/array_of_bool_as_bitvec/main.c b/regression/cbmc/array_of_bool_as_bitvec/main.c deleted file mode 100644 index 19888bb1a45..00000000000 --- a/regression/cbmc/array_of_bool_as_bitvec/main.c +++ /dev/null @@ -1,19 +0,0 @@ -#include -#include -#include - -__CPROVER_bool w[8]; - -void main() -{ - _Bool x[8] = {false}; - __CPROVER_bool y[8] = {false}; - bool *z = calloc(8, sizeof(bool)); - - unsigned idx; - __CPROVER_assume(0 <= idx && idx < 8); - - assert(w[idx] == x[idx]); - assert(x[idx] == y[idx]); - assert(y[idx] == z[idx]); -} diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc deleted file mode 100644 index ae228a04e44..00000000000 --- a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc +++ /dev/null @@ -1,31 +0,0 @@ -CORE broken-smt-backend -main.c ---smt2 --outfile - -\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\) -\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\) -\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\) -^EXIT=0$ -^SIGNAL=0$ --- -\(= \(select array_of\.2 i\) false\) -\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\) -\(= \(select array\.3 \(_ bv\d+ 64\)\) false\) --- -This test checks for correctness of BitVec-array encoding of Boolean arrays. - -Ideally, we shouldn't have to check the SMT output, but should run with backend -SMT solvers. However, we currently cannot because of #5977 (also see #6005). - -For now, we tag this test as `broken-smt-backend` to avoid running main.c -with `--z3` or `--cprover-smt2`, both of which encode Boolean arrays directly. -Instead, we generate a generic SMT encoding with `--smt2` and check the output. - -Explanation of regexes: -line 4,10: array.2 elements should be BitVec not Bool -line 5,11: equality operator (=) should have 2 arguments not 3 -line 6,12: array.3 elements should be BitVec not Bool - -Once #5977 and #6005 are resolved, we should: -- remove `broken-smt-backend` tag -- run with `--smt2 --cprover-smt2` and `--smt2 --z3` -- check for successful verification diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 93cd707ff48..9435c2196a6 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -59,7 +59,6 @@ smt2_convt::smt2_convt( solvert _solver, std::ostream &_out) : use_FPA_theory(false), - use_array_of_bool(false), use_as_const(false), use_check_sat_assuming(false), use_datatypes(false), @@ -88,7 +87,6 @@ smt2_convt::smt2_convt( case solvert::CPROVER_SMT2: use_FPA_theory = true; - use_array_of_bool = true; use_as_const = true; use_check_sat_assuming = true; emit_set_logic = false; @@ -99,7 +97,6 @@ smt2_convt::smt2_convt( case solvert::CVC4: logic = "ALL"; - use_array_of_bool = true; use_as_const = true; break; @@ -110,7 +107,6 @@ smt2_convt::smt2_convt( break; case solvert::Z3: - use_array_of_bool = true; use_as_const = true; use_check_sat_assuming = true; use_lambda_for_array = true; @@ -4070,24 +4066,11 @@ void smt2_convt::convert_index(const index_exprt &expr) if(use_array_theory(expr.array())) { - if(expr.type().id() == ID_bool && !use_array_of_bool) - { - out << "(= "; - out << "(select "; - convert_expr(expr.array()); - out << " "; - convert_expr(typecast_exprt(expr.index(), array_type.size().type())); - out << ")"; - out << " #b1)"; - } - else - { - out << "(select "; - convert_expr(expr.array()); - out << " "; - convert_expr(typecast_exprt(expr.index(), array_type.size().type())); - out << ")"; - } + out << "(select "; + convert_expr(expr.array()); + out << " "; + convert_expr(typecast_exprt(expr.index(), array_type.size().type())); + out << ")"; } else { @@ -4644,16 +4627,7 @@ void smt2_convt::find_symbols(const exprt &expr) out << "(assert (forall ((i "; convert_type(array_type.size().type()); out << ")) (= (select " << id << " i) "; - if(array_type.element_type().id() == ID_bool && !use_array_of_bool) - { - out << "(ite "; - convert_expr(array_of.what()); - out << " #b1 #b0)"; - } - else - { - convert_expr(array_of.what()); - } + convert_expr(array_of.what()); out << ")))\n"; defined_expressions[expr] = id; @@ -4692,16 +4666,7 @@ void smt2_convt::find_symbols(const exprt &expr) out << ")) (= (select " << id << " "; convert_expr(array_comprehension.arg()); out << ") "; - if(array_type.element_type().id() == ID_bool && !use_array_of_bool) - { - out << "(ite "; - convert_expr(array_comprehension.body()); - out << " #b1 #b0)"; - } - else - { - convert_expr(array_comprehension.body()); - } + convert_expr(array_comprehension.body()); out << "))))\n"; defined_expressions[expr] = id; @@ -4725,16 +4690,7 @@ void smt2_convt::find_symbols(const exprt &expr) out << "(assert (= (select " << id << " "; convert_expr(from_integer(i, array_type.size().type())); out << ") "; // select - if(array_type.element_type().id() == ID_bool && !use_array_of_bool) - { - out << "(ite "; - convert_expr(expr.operands()[i]); - out << " #b1 #b0)"; - } - else - { - convert_expr(expr.operands()[i]); - } + convert_expr(expr.operands()[i]); out << "))" << "\n"; // =, assert } @@ -4879,17 +4835,10 @@ void smt2_convt::convert_type(const typet &type) CHECK_RETURN(array_type.size().is_not_nil()); // we always use array theory for top-level arrays - const typet &subtype = array_type.element_type(); - out << "(Array "; convert_type(array_type.size().type()); out << " "; - - if(subtype.id()==ID_bool && !use_array_of_bool) - out << "(_ BitVec 1)"; - else - convert_type(array_type.element_type()); - + convert_type(array_type.element_type()); out << ")"; } else if(type.id()==ID_bool) diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index ef6cffe1be0..efb3e2cf4c9 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -58,7 +58,6 @@ class smt2_convt : public stack_decision_proceduret ~smt2_convt() override = default; bool use_FPA_theory; - bool use_array_of_bool; bool use_as_const; bool use_check_sat_assuming; bool use_datatypes;