use FPA theory when generating SMT-LIB2 for Z3

This enables the use of the FPA theory when generating SMT-LIB2 for Z3.

This is already the default when using Bitwutzla or CVC 5.

Author: kroening

CHANGELOG

@@ -1,11 +1,10 @@
 # EBMC 6.0
-* VCD traces now written into separate files per property
 
+* VCD traces now written into separate files per property
 * SMV: removed legacy keywords EXTERN and switch
-
 * SMV: use NuSMV's operator precedence, as opposed to CMU SMV's
-
 * SystemVerilog: semantics fix for cover disable iff
+* Now uses the FPA theory when emitting SMT-LIB for Z3
 
 # EBMC 5.11
 

regression/verilog/expressions/cast_from_real1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 cast_from_real1.sv
 
 ^EXIT=0$

regression/verilog/expressions/cast_to_real1.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 cast_to_real1.sv
 
 ^EXIT=0$

src/ebmc/ebmc_solver_factory.cpp

@@ -90,6 +90,9 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
           smt2_solver.value(),
           output_file_ptr->stream());
 
+        if(smt2_solver == smt2_convt::solvert::Z3)
+          dec->use_FPA_theory = true;
+
         return ebmc_solvert{std::move(output_file_ptr), std::move(dec)};
       };
     }
@@ -118,14 +121,19 @@ ebmc_solver_factoryt ebmc_solver_factory(const cmdlinet &cmdline)
         }
         else
         {
-          return ebmc_solvert{std::make_unique<smt2_dect>(
+          auto dec = std::make_unique<smt2_dect>(
             ns,
             "ebmc",
             std::string("Generated by EBMC ") + EBMC_VERSION,
             "QF_AUFBV",
             smt2_solver.value(),
             "", // solver binary
-            message_handler)};
+            message_handler);
+
+          if(smt2_solver == smt2_convt::solvert::Z3)
+            dec->use_FPA_theory = true;
+
+          return ebmc_solvert{std::move(dec)};
         }
       };
   }