From e8ef9a85a4681ee82f53d838e03bfb0f012f83c9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 26 Jul 2020 13:22:06 -0700
Subject: [PATCH] fix #4327

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_solver.cpp | 4 ++++
 src/smt/theory_lra.cpp | 4 +++-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index fb586cafb..84d9894fc 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -134,6 +134,10 @@ namespace {
 
         void collect_param_descrs(param_descrs & r) override {
             m_context.collect_param_descrs(r);
+            insert_timeout(r);
+            insert_rlimit(r);
+            insert_max_memory(r);
+            insert_ctrl_c(r);
         }
 
         void collect_statistics(statistics & st) const override {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ee6a7c8d1..101f74bf9 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1738,6 +1738,7 @@ public:
             TRACE("arith", /*display(tout);*/
                   ctx().display(tout);
                   );
+
             switch (check_lia()) {
             case l_true:
                 break;
@@ -1748,7 +1749,7 @@ public:
                 st = FC_CONTINUE;
                 break;
             }
-            
+
             switch (check_nla()) {
             case l_true:
                 break;
@@ -1759,6 +1760,7 @@ public:
                 st = FC_GIVEUP;
                 break;
             }
+            
             if (delayed_assume_eqs()) {
                 ++m_stats.m_assume_eqs;
                 return FC_CONTINUE;