Alternative bdd -> exprt translation expanding ID_if

Quantifier flatting presently cannot cope with ID_if.

Author: tautschnig

src/solvers/prop/bdd_expr.cpp

@@ -132,7 +132,14 @@ exprt bdd_exprt::as_expr(const mini_bddt &r) const
   else if(r.high().is_true())
     return or_exprt(n_expr, as_expr(r.low()));
   else
+    #if 0
+    return
+      and_exprt(
+        or_exprt(not_exprt(n_expr), as_expr(r.high())),
+        or_exprt(n_expr, as_expr(r.low())));
+    #else
     return if_exprt(n_expr, as_expr(r.high()), as_expr(r.low()));
+    #endif
 }
 
 exprt bdd_exprt::as_expr() const