diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2020-12-17 17:12:15 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-17 17:12:15 +0100 |
| commit | 1753106f61bca87513a84493b643e2a7e245e0f5 (patch) | |
| tree | d2d24cb98a66c06a3c533eaaa56ed6462c9c713b /src/theory/arith/theory_arith.cpp | |
| parent | bdcb62974f553acd47fdb04f8d95725489328139 (diff) | |
(proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697)
This PR prepares the nonlinear extension itself and the nl-ext part for proofs. In particular
we add a proof checker for nl-ext
we add a CDProofSet for nl-ext
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b8cead4fc..d1dd4bb63 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -82,7 +82,7 @@ void TheoryArith::finishInit() if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) { d_nonlinearExtension.reset( - new nl::NonlinearExtension(*this, d_astate, d_equalityEngine)); + new nl::NonlinearExtension(*this, d_astate, d_equalityEngine, d_pnm)); } // finish initialize internally d_internal->finishInit(); |