diff --git a/src/math/dd/dd_fdd.cpp b/src/math/dd/dd_fdd.cpp
index f67ba5069..5aec00351 100644
--- a/src/math/dd/dd_fdd.cpp
+++ b/src/math/dd/dd_fdd.cpp
@@ -215,10 +215,9 @@ namespace dd {
         }
 
         SASSERT(!lo[idx]);
-        trail.reverse();
         lo[idx] = true;
         unsigned v = m_pos2var[idx];
-        b = trail[idx].cofactor(m->mk_var(v));
+        b = trail[lo.size() - idx - 1].cofactor(m->mk_var(v));
         for (unsigned i = idx; i-- > 0; ) {
             SASSERT(!b.is_true());
             if (b.is_false()) {
@@ -235,7 +234,7 @@ namespace dd {
 
         dec(lo);
         
-	return true;
+	    return true;
     }
     
     bool fdd::inf(bdd const& x, bool_vector& hi) const {
@@ -279,12 +278,10 @@ namespace dd {
         }
 
         SASSERT(hi[idx]);
-        trail.reverse();
         hi[idx] = false;
         unsigned v = m_pos2var[idx];
-        b = trail[idx].cofactor(m->mk_nvar(v));
+        b = trail[hi.size() - idx - 1].cofactor(m->mk_nvar(v));
 
-        // Check logic, TBD
         for (unsigned i = idx; i-- > 0; ) {
             SASSERT(!b.is_true());
             if (b.is_false()) {
@@ -292,11 +289,11 @@ namespace dd {
                     hi[j] = true;
                 break;
             }
-            hi[i] = b.lo().is_true();
-            if (hi[i]) 
-                b = b.hi();
-            else 
+            hi[i] = !b.hi().is_true();
+            if (!hi[i]) 
                 b = b.lo();
+            else 
+                b = b.hi();
         }
 
         inc(hi);
diff --git a/src/test/bdd.cpp b/src/test/bdd.cpp
index d7b4ef3fb..9f297337e 100644
--- a/src/test/bdd.cpp
+++ b/src/test/bdd.cpp
@@ -446,6 +446,14 @@ public:
         }
     }
 
+    static void dec(bool_vector& x) {
+        for (auto& b : x) {
+            b = !b;
+            if (!b)
+                break;
+        }
+    }
+
     static unsigned value(bool_vector const& x) {
         unsigned p = 1;
         unsigned v = 0;
@@ -463,15 +471,42 @@ public:
         bddv const& x = x_dom.var();
         bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33);
         bool_vector lo(10, false);
-        for (unsigned i = 0; i < 30; ++i) {
+        for (unsigned i = 0; i < 20; ++i) {
+            unsigned v = value(lo);
             bool found = x_dom.sup(c, lo);
-            std::cout << found << ": " << value(lo) << "\n";
+            std::cout << found << ": " << v << " - " << value(lo) << "\n";
             if (found) 
                 std::cout << x_dom.sup(c, lo) << ": " << value(lo) << "\n";
+            c = !c;
             inc(lo);
         }        
     }
 
+    static void test_inf() {
+	std::cout << "test_inf\n";
+	bdd_manager m(20);
+        fdd const x_dom(m, 10);
+        bddv const& x = x_dom.var();
+        bdd c = (1 <= x && x <= 5) || (11 <= x && x <= 13) || (29 <= x && x <= 33);
+        bool_vector hi(10, true);
+        for (unsigned i = 0; i < 10; ++i) {
+            bool found = x_dom.inf(c, hi);
+            std::cout << found << ": " << value(hi) << "\n";
+            if (found) {
+                std::cout << x_dom.inf(c, hi) << ": " << value(hi) << "\n";
+                SASSERT(value(hi) == 0 || value(hi) == 1 || value(hi) == 5 || value(hi) == 6 ||
+                        value(hi) == 10 || value(hi) == 11 || 
+                        value(hi) == 13 || value(hi) == 14 || 
+                        value(hi) == 28 || value(hi) == 29 || 
+                        value(hi) == 33 || value(hi) == 34 || value(hi) == 1023);
+            }
+            c = !c;
+            dec(hi);
+        }        
+    }
+
+
+
 };
 
 }
@@ -494,5 +529,6 @@ void tst_bdd() {
     dd::test_bdd::test_fdd_twovars();
     dd::test_bdd::test_fdd_find_hint();
     dd::test_bdd::test_cofactor();
+    dd::test_bdd::test_inf();
     dd::test_bdd::test_sup();
 }