From a9dccb878cef1bab897e182a6c0365e333191dd5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 2 Jun 2018 13:39:20 -0500 Subject: [PATCH] Fix corner case of mixed int/real cegqi. (#2046) --- src/theory/arith/arith_msum.cpp | 1 + src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp index 46ee1cad5..c56587901 100644 --- a/src/theory/arith/arith_msum.cpp +++ b/src/theory/arith/arith_msum.cpp @@ -148,6 +148,7 @@ Node ArithMSum::mkNode(const std::map& msum) int ArithMSum::isolate( Node v, const std::map& msum, Node& veq_c, Node& val, Kind k) { + Assert(veq_c.isNull()); std::map::const_iterator itv = msum.find(v); if (itv != msum.end()) { diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp index 203697fd7..0274d45cd 100644 --- a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp @@ -198,6 +198,7 @@ int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, No Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) ); //re-isolate Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; + veq_c = Node::null(); ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); Trace("cegqi-arith-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; Trace("cegqi-arith-debug") << " real part : " << realPart << std::endl; -- 2.30.2