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 ff1962629096f6b5c86ce3e96af9c4659e10f574..3c46e165253dbfb1f141fbe2e41c34cb847e956a 100644 (file)
--- 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();