diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-01 09:53:46 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-01 14:53:46 +0000 |
| commit | e56900bcacd2698de70172d9c1c79f32a1cbb0eb (patch) | |
| tree | 549aaa19bbfd48d0f4e92d3f4e91f906bf8a3fce /src/theory/arith/nl/nonlinear_extension.cpp | |
| parent | b371364633912a681696eb7bda4a631a74b0539d (diff) | |
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.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
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(); |