diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-02 13:39:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-02 13:39:20 -0500 |
| commit | a9dccb878cef1bab897e182a6c0365e333191dd5 (patch) | |
| tree | 117fa9ba40e46cb499bc2c568122bcc540022c58 /src/theory/quantifiers/cegqi | |
| parent | d440c5f3bea930c4f30d62858b878ab36c676312 (diff) | |
Fix corner case of mixed int/real cegqi. (#2046)
Diffstat (limited to 'src/theory/quantifiers/cegqi')
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
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; |