#5454

@wintersteiger: added code review comment to theory_fpa. The bug seen in #5454 doesn't surface with theory_fpa, though.

src/ast/fpa/fpa2bv_converter.cpp

@@ -19,6 +19,7 @@ Notes:
 #include<math.h>
 
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_pp.h"
 #include "ast/well_sorted.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/used_vars.h"
@@ -4430,7 +4431,7 @@ expr* fpa2bv_converter_wrapped::bv2fpa_value(sort* s, expr* a, expr* b, expr* c)
     mpfm.set(f, ebits, sbits, mpzm.is_one(sgn_z), mpzm.get_int64(exp_u), sig_z);
     result = m_util.mk_value(f);
 
-    TRACE("t_fpa", tout << "result: [" <<
+    TRACE("t_fpa", tout << mk_pp(a, m) << " " << mk_pp(b, m) << " " << mk_pp(c, m) << " result: [" <<
           mpzm.to_string(sgn_z) << "," <<
           mpzm.to_string(exp_z) << "," <<
           mpzm.to_string(sig_z) << "] --> " <<

src/sat/smt/fpa_solver.cpp

@@ -83,6 +83,12 @@ namespace fpa {
         return conds;
     }
 
+    sat::check_result solver::check() {
+        SASSERT(m_converter.m_extra_assertions.empty());
+        SASSERT(m_nodes.size() <= m_nodes_qhead);
+        return sat::check_result::CR_DONE;
+    }
+
     void solver::attach_new_th_var(enode* n) {
         theory_var v = mk_var(n);
         ctx.attach_th_var(n, this, v);
@@ -183,7 +189,7 @@ namespace fpa {
                 add_unit(atom);
             }
         }
-        else {
+        else {            
             switch (a->get_decl_kind()) {
             case OP_FPA_TO_FP:
             case OP_FPA_TO_UBV:
@@ -199,7 +205,7 @@ namespace fpa {
                 break;
             }
         }
-
+        activate(e);
     }
 
     void solver::activate(expr* n) {
@@ -223,7 +229,11 @@ namespace fpa {
                     VERIFY(m_fpa_util.is_fp(bv_val_e, a, b, c));
                     expr* args[] = { a, b, c };
                     expr_ref cc_args(m_bv_util.mk_concat(3, args), m);
+                    // Require
+                    // wrap(n) = bvK
+                    // fp(extract(wrap(n)) = n
                     add_unit(eq_internalize(wrapped, cc_args));
+                    add_unit(eq_internalize(bv_val_e, n));
                     add_units(mk_side_conditions());
                 }
                 else if (m.is_ite(n)) {
@@ -313,6 +323,7 @@ namespace fpa {
         expr* e = n->get_expr();
         app_ref wrapped(m);
         expr_ref value(m);
+        
         auto is_wrapped = [&]() {
             if (!wrapped) wrapped = m_converter.wrap(e);
             return expr2enode(wrapped) != nullptr;
@@ -345,6 +356,7 @@ namespace fpa {
             value = m_fpa_util.mk_pzero(ebits, sbits);
         }
         values.set(n->get_root_id(), value);
+        TRACE("t_fpa", tout << ctx.bpp(n) << " := " << value << "\n";);
     }
 
     bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {

src/sat/smt/fpa_solver.h

@@ -72,7 +72,7 @@ namespace fpa {
 
         bool unit_propagate() override;
         void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); }
-        sat::check_result check() override { return sat::check_result::CR_DONE; }
+      sat::check_result check() override;
 
         euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); }
 

src/smt/theory_fpa.cpp

@@ -454,6 +454,11 @@ namespace smt {
                     expr * args[] = { bv_val_a->get_arg(0), bv_val_a->get_arg(1), bv_val_a->get_arg(2) };
                     cc_args = m_bv_util.mk_concat(3, args);
                     c = m.mk_eq(wrapped, cc_args);
+		    // NB code review: #5454 exposes a bug in fpa_solver that
+		    // could be latent here as well. It needs also the equality
+		    // n == bv_val_e to be asserted such that whenever something is assigned th
+		    // bit-vector value cc_args it is equated with n
+		    // I don't see another way this constraint would be enforced.
                     assert_cnstr(c);
                     assert_cnstr(mk_side_conditions());
                 }