From 770d9ae622ec04bc2fbea8356ce11329ed06fa5b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 23 Sep 2020 20:05:06 +0200 Subject: Make IAND solver use inference manager. (#5126) This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas. --- src/theory/arith/theory_arith.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/arith/theory_arith.cpp') diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index abdf6930a..9324c94af 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -83,7 +83,7 @@ void TheoryArith::finishInit() if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) { d_nonlinearExtension.reset( - new nl::NonlinearExtension(*this, d_equalityEngine)); + new nl::NonlinearExtension(*this, d_astate, d_equalityEngine)); } // finish initialize internally d_internal->finishInit(); -- cgit v1.2.3