Ensure nonlinear extensions properly reconsiders its model (#6204)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 25 Mar 2021 20:40:58 +0000 (21:40 +0100)
committerGitHub <noreply@github.com>
Thu, 25 Mar 2021 20:40:58 +0000 (20:40 +0000)
commitfa6c3db414d27f47e0bee55480df939e78c14eb3
tree6c4e69973a078b3bd29c212c1d9945cbba0f5497
parent99a74de90a064133a8e3d03ee9334d59be34ba1d
Ensure nonlinear extensions properly reconsiders its model (#6204)

In certain cases, the nonlinear extension would not re-check properly but only repeat an (already failed) model repair. The result lemma would then already be in cache and thus not be sent to the solver.
This PR ensures that modelBasedRefinement is always run and entirely removes the d_builtModel flag that was responsible for this behavior. Additionally, it asserts that the lemma that (tries to) force the model to be reconciled during theory combination is actually sent.
Fixes #6192.
src/theory/arith/nl/nonlinear_extension.cpp
src/theory/arith/nl/nonlinear_extension.h
src/theory/arith/theory_arith.cpp