Undefined atom polarity triggers assertion

[cgd8d]

I run the following:

$ cat ReproducePatch1Bug.smt2
(set-logic QF_NRA)
(set-info :precision 0.00001)

(declare-fun x () Real [-1, 2])
(declare-fun forall w () Real [-3.141593, 3.141593])
(assert (
        forall (
                (w Real)
        )
(or (< (cos w) 0.3) (<= 0.4 x))
))
(check-sat)
(exit)
$ ./dreal3/build/debug/dReal --polytope ReproducePatch1Bug.smt2
dReal: /home/davis/software/dreal3_20170327/dreal3/src/contractor/contractor_ibex.cpp:109: ibex::SystemFactory* dreal::contractor_ibex_polytope::build_system_factory(const std::vector<Enode*>&, const std::vector<std::shared_ptr<dreal::nonlinear_constraint> >&): Assertion `p == l_True || p == l_False' failed.
Aborted (core dumped)

I believe the issue is that atoms which are created in dreal::strengthen_enode have an undefined polarity, whereas dreal::contractor_ibex_polytope::build_system_factory requires polarity to place enodes into the correct cache. I’m fuzzy on what exactly should be happening here (not sure I fully understand the semantics behind polarity), but the issue seems to be fixed by forcing the atoms created by strengthen_enode to true with the following patch:

$ git diff src/util/enode_utils.cpp
diff --git a/src/util/enode_utils.cpp b/src/util/enode_utils.cpp
index 5e593fa..1d189b7 100644
--- a/src/util/enode_utils.cpp
+++ b/src/util/enode_utils.cpp
@@ -227,25 +227,40 @@ Enode * strengthen_enode(Egraph & eg, Enode * const e, double const eps, bool co
         // doesn't provide enough pruning power.
         // We're using (e1 - e2)^2 >= eps^2 encoding.
         Enode * const eps_node_sq = eg.mkNum(eps * eps);
-        return eg.mkGeq(eg.cons(eg.mkPow(eg.cons(eg.mkMinus(e1, e2), eg.cons(eg.mkNum(2.0)))),
+        Enode* ret = eg.mkGeq(eg.cons(eg.mkPow(eg.cons(eg.mkMinus(e1, e2), eg.cons(eg.mkNum(2.0)))),
                                 eg.cons(eps_node_sq)));
+        assert(ret->isTAtom());
+        if (!ret->hasPolarity()) ret->setPolarity(true);
+        return ret;
     }
     Enode * const eps_node = eg.mkNum(eps);
     if ((polarity && e->isLt()) || (!polarity && e->isGeq())) {
         // e1 <  e2  ==>  e1 < e2 - eps
-        return eg.mkLt(eg.cons(e1, eg.cons(eg.mkMinus(e2, eps_node))));
+        Enode* ret = eg.mkLt(eg.cons(e1, eg.cons(eg.mkMinus(e2, eps_node))));
+        assert(ret->getCdr()->getCar()->isTAtom());
+        if (!ret->getCdr()->getCar()->hasPolarity()) ret->getCdr()->getCar()->setPolarity(true);
+        return ret;
     }
     if ((polarity && e->isLeq()) || (!polarity && e->isGt())) {
        // e1 <= e2  ==>  e1 <= e2 - eps
-        return eg.mkLeq(eg.cons(e1, eg.cons(eg.mkMinus(e2, eps_node))));
+        Enode* ret = eg.mkLeq(eg.cons(e1, eg.cons(eg.mkMinus(e2, eps_node))));
+        assert(ret->isTAtom());
+        if (!ret->hasPolarity()) ret->setPolarity(true);
+        return ret;
     }
     if ((polarity && e->isGt()) || (!polarity && e->isLeq())) {
         // e1 >  e2  ==>  e1 > e2 + eps
-        return eg.mkGt(eg.cons(e1, eg.cons(eg.mkPlus(e2, eps_node))));
+        Enode* ret = eg.mkGt(eg.cons(e1, eg.cons(eg.mkPlus(e2, eps_node))));
+        assert(ret->getCdr()->getCar()->isTAtom());
+        if (!ret->getCdr()->getCar()->hasPolarity()) ret->getCdr()->getCar()->setPolarity(true);
+        return ret;
     }
     if ((polarity && e->isGeq()) || (!polarity && e->isLt())) {
         // e1 >= e2  ==>  e1 >= e2 + eps
-        return eg.mkGeq(eg.cons(e1, eg.cons(eg.mkPlus(e2, eps_node))));
+        Enode* ret = eg.mkGeq(eg.cons(e1, eg.cons(eg.mkPlus(e2, eps_node))));
+        assert(ret->isTAtom());
+        if (!ret->hasPolarity()) ret->setPolarity(true);
+        return ret;
     }
     // Something is wrong.
     ostringstream os;