diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-29 14:38:19 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-29 07:38:19 -0500 |
| commit | 8431e9d49b71774092ca29c85855cbdf5bf09c53 (patch) | |
| tree | bcd71d6e0526282331c8e62e657f530eb68da86e /src/smt/term_formula_removal.cpp | |
| parent | 9e5a4a3e6aca1b25cf1af4a6392003cb5ecb8866 (diff) | |
Avoid exponential explosion of small constant in CEGQI (#6461)
This PR fixes an issue that can lead to an exponential explosion of a rational constant for repeated calls to the cegqi instantiation strategy. The d_small_const variable was squared regularly, we now simply multiply it with its original value.
Diffstat (limited to 'src/smt/term_formula_removal.cpp')
0 files changed, 0 insertions, 0 deletions