diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2020-12-18 08:26:55 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-18 08:26:55 +0100 |
| commit | 0ae11d1abec9017784eefa2252d8e8ea7dfb4f74 (patch) | |
| tree | eaca05442c315dcd9956047ebb6f5eaa63c56102 /src/theory/arith/nl/nonlinear_extension.cpp | |
| parent | 9b099b715cec0dc60048fdc64b4d61b977d14096 (diff) | |
Add proof for split zero check. (#5699)
This PR adds a proof for the nl-ext check to split at zero. As we can use the SPLIT rule, this requires no new proof rule.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index e4a71b34d..d52095e95 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -52,7 +52,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_factoringSlv(d_im, d_model), d_monomialBoundsSlv(&d_extState), d_monomialSlv(&d_extState), - d_splitZeroSlv(&d_extState, state.getUserContext()), + d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), d_cadSlv(d_im, d_model), d_icpSlv(d_im), |