diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-24 16:24:25 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-24 15:24:25 +0000 |
| commit | cfe207563479a1e9e13d52bdd93446a8c816636a (patch) | |
| tree | b627d7b238df9ba500cc63ef7ddee62f3bc96d3f /src/theory/quantifiers/conjecture_generator.cpp | |
| parent | 31bba4ba83354f41c756e9800489672ff1c9711c (diff) | |
Only consider relevant terms for integer branches (#6181)
Linear arithmetic simply tried to branch on the first integer variable that had a non-integral assignment.
If it holds stale variables that are not part of the current input, these branches can be emitted and are processed by the solver, but the resulting new assertions will not be considered relevant and thus not added to the theory.
As it still triggers a new theory check, linear arithmetic repeats the same procedure and causes an infinite loop.
This PR explicitly tracks the currently relevant nodes by storing all preregistered nodes and only allows branching on variables from this set.
Fixes #6146.
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.cpp')
0 files changed, 0 insertions, 0 deletions