Swap logic set to include arrays

So that we can use array theory.

Author: thomasspriggs

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

@@ -3,7 +3,7 @@ control_flow.c
 --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 - \(set-logic QF_AUFBV\)
 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\)\)

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

@@ -3,7 +3,7 @@ test.c
 --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 - \(set-logic QF_AUFBV\)
 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|\)\)

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -140,7 +140,7 @@ smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret(
   solver_process->send(
     smt_set_option_commandt{smt_option_produce_modelst{true}});
   solver_process->send(smt_set_logic_commandt{
-    smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
+    smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}});
   solver_process->send(object_size_function.declaration);
 }
 

src/solvers/smt2_incremental/smt_logics.def

@@ -10,5 +10,5 @@ LOGIC_ID(quantifier_free_uninterpreted_functions, QF_UF)
 LOGIC_ID(quantifier_free_bit_vectors, QF_BV)
 LOGIC_ID(quantifier_free_uninterpreted_functions_bit_vectors, QF_UFBV)
 LOGIC_ID(quantifier_free_bit_vectors_arrays, QF_ABV)
-LOGIC_ID(quantifier_free_uninterpreted_functions_bit_vectors_arrays, QF_AUFBV)
+LOGIC_ID(quantifier_free_arrays_uninterpreted_functions_bit_vectors, QF_AUFBV)
 LOGIC_ID(all, ALL)

unit/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -170,7 +170,8 @@ TEST_CASE(
       std::vector<smt_commandt>{
         smt_set_option_commandt{smt_option_produce_modelst{true}},
         smt_set_logic_commandt{
-          smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}},
+          // NOLINTNEXTLINE(whitespace/line_length)
+          smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{}},
         test.object_size_function.declaration});
     test.sent_commands.clear();
     SECTION("Set symbol to true.")

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -196,7 +196,7 @@ TEST_CASE(
   const auto qf_abv = smt_logic_quantifier_free_bit_vectors_arrayst{};
   CHECK(smt_to_smt2_string(qf_abv) == "QF_ABV");
   const auto qf_aufbv =
-    smt_logic_quantifier_free_uninterpreted_functions_bit_vectors_arrayst{};
+    smt_logic_quantifier_free_arrays_uninterpreted_functions_bit_vectorst{};
   CHECK(smt_to_smt2_string(qf_aufbv) == "QF_AUFBV");
   CHECK(smt_to_smt2_string(smt_logic_allt{}) == "ALL");
   CHECK(