diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-08-26 07:19:56 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-26 14:19:56 +0000 |
| commit | daee9d4ec0c9e7c5054345c4156c4debe815e045 (patch) | |
| tree | 0592cd34886c85af2dcf7e962c6f8a68006f748b /src/theory/builtin | |
| parent | a81064b538382670f25c87f138961f12def7880a (diff) | |
Improve integration of nonlinear arithmetic into the arithmetic theory. (#6956)
The nonlinear extension used to be called only during model construction, a rather atypical place which lead to a series of subtle issues. This PR moves it into the postCheck method. To do that, a few other changes are necessary, most notably collectAssertedTerms and collectTerms are moved back from the model manager into the theory class.
Diffstat (limited to 'src/theory/builtin')
0 files changed, 0 insertions, 0 deletions