Add unit test for BDD

This adds a test case to check there are no mistakes in the BDD to expr
conversions.
This test can fail without the previous fix.

Author: romainbrenguier

unit/solvers/prop/bdd_expr.cpp

@@ -44,4 +44,23 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]")
       REQUIRE(bdd.as_expr() == bdd2.as_expr());
     }
   }
+
+  GIVEN("A bdd for (a&!b)")
+  {
+    const symbol_exprt a("a", bool_typet());
+    const symbol_exprt b("b", bool_typet());
+
+    const bddt bdd = bdd_expr_converter.from_expr(and_exprt(a, not_exprt(b)));
+
+    WHEN("It is converted to an exprt")
+    {
+      const exprt result = bdd_expr_converter.as_expr(bdd);
+      THEN("It is equal to the expression (a & !b) or (!b & a)")
+      {
+        const bool correct = result == and_exprt(a, not_exprt(b)) ||
+                             result == and_exprt(not_exprt(b), a);
+        REQUIRE(correct);
+      }
+    }
+  }
 }