Fix corner case of mixed int/real cegqi. (#2046)

diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index 46ee1cad5dc8e41471b62395b2cdb6f063d0a2a5..c56587901d53df28983943f2f9786c79d7d827f5 100644 (file)
--- a/src/theory/arith/arith_msum.cpp
+++ b/src/theory/arith/arith_msum.cpp
@@ -148,6 +148,7 @@ Node ArithMSum::mkNode(const std::map<Node, Node>& msum)
 int ArithMSum::isolate(
     Node v, const std::map<Node, Node>& msum, Node& veq_c, Node& val, Kind k)
 {
+  Assert(veq_c.isNull());
   std::map<Node, Node>::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 203697fd7cf6ae4e00d4a454c76d2bebe120092b..0274d45cd8d3a29d28cbe5a19a31001d9c7edc4d 100644 (file)
--- 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;