From 7bae29729799acd401fc567d2ba90ff0ed6b8101 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 24 Aug 2021 11:24:31 -0700
Subject: [PATCH] #5482

add unit propagation
---
 src/sat/smt/fpa_solver.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp
index d32671182..f655a0241 100644
--- a/src/sat/smt/fpa_solver.cpp
+++ b/src/sat/smt/fpa_solver.cpp
@@ -85,6 +85,8 @@ namespace fpa {
 
     sat::check_result solver::check() {
         SASSERT(m_converter.m_extra_assertions.empty());
+        if (unit_propagate())
+            return sat::check_result::CR_CONTINUE;
         SASSERT(m_nodes.size() <= m_nodes_qhead);
         return sat::check_result::CR_DONE;
     }
@@ -165,7 +167,6 @@ namespace fpa {
     }
 
     bool solver::unit_propagate() {
-
         if (m_nodes.size() <= m_nodes_qhead)
             return false;
         ctx.push(value_trail<unsigned>(m_nodes_qhead));