diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index 18d3d5ede06..71a311e31a9 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -126,10 +126,9 @@ class bdd_propt : public propt return {}; } - literalt lselect(literalt, literalt, literalt) override + literalt lselect(literalt c, literalt t, literalt f) override { - UNREACHABLE; - return {}; + return to_literal((to_bdd(!c) | to_bdd(t)) & (to_bdd(c) | to_bdd(f))); } void lcnf(const bvt &) override