From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 1 Apr 2021 14:53:46 +0000 (-0500)
Subject: Fix non-linear for unknown case (#6252)
X-Git-Tag: cvc5-1.0.0~1995
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e56900bcacd2698de70172d9c1c79f32a1cbb0eb;p=cvc5.git

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.
---

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();