From e56900bcacd2698de70172d9c1c79f32a1cbb0eb Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 1 Apr 2021 09:53:46 -0500
Subject: Fix non-linear for unknown case (#6252)

As a result of this issue, currently we are incorrectly trying to repair a model when one is not guaranteed to exist, leading to a spurious assertion failure.

Fixes #6228. The benchmarks on that issue now answer "unknown" without an assertion failure.
---
 src/theory/arith/nl/nonlinear_extension.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index ff1962629..3c46e1652 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -490,6 +490,7 @@ Result::Sat NonlinearExtension::modelBasedRefinement(const std::set<Node>& termS
                            "NonLinearExtension, set incomplete"
                         << std::endl;
         d_containing.getOutputChannel().setIncomplete();
+        return Result::Sat::SAT_UNKNOWN;
       }
     }
     d_im.clearWaitingLemmas();
-- 
cgit v1.2.3