From 2fa156eaf40f4b61a0632adbed884a90fd215925 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 25 Jul 2021 09:36:45 -0700
Subject: [PATCH] #5429

---
 src/sat/smt/array_solver.cpp | 1 +
 src/sat/smt/fpa_solver.cpp   | 5 ++++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/array_solver.cpp b/src/sat/smt/array_solver.cpp
index 4e6f75c4d..bb588948e 100644
--- a/src/sat/smt/array_solver.cpp
+++ b/src/sat/smt/array_solver.cpp
@@ -176,6 +176,7 @@ namespace array {
         TRACE("array", tout << "v" << v_child << " - " << ctx.bpp(select) << " " << ctx.bpp(child) << " prop: " << should_prop_upward(get_var_data(v_child)) << "\n";);
         if (can_beta_reduce(child)) 
             push_axiom(select_axiom(select, child));
+	    propagate_parent_select_axioms(v_child);
     }
 
     void solver::add_lambda(theory_var v, euf::enode* lambda) {
diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index 42e3f8726..13837d0ce 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -93,7 +93,10 @@ namespace fpa {
         SASSERT(m.is_bool(e));
         if (!visit_rec(m, e, sign, root, redundant))
             return sat::null_literal;
-        return expr2literal(e);
+        sat::literal lit = expr2literal(e);
+        if (sign)
+           lit.neg();
+        return lit;
     }
 
     void solver::internalize(expr* e, bool redundant) {