Fix bdd.as_expr()

romainbrenguier · romainbrenguier · commit 6406fdfc0ab9 · 2019-02-25T16:16:55.000Z
There was a mistake in the way complement is computed when going to the
then_branch.
diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp
@@ -119,11 +119,14 @@ exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const
       if(r.else_branch().is_complement() != complement)
       {
         return and_exprt(
-          n_expr, as_expr(r.then_branch(), complement != r.is_complement()));
+          n_expr,
+          as_expr(
+            r.then_branch(), complement != r.then_branch().is_complement()));
       }
       return or_exprt(
         not_exprt(n_expr),
-        as_expr(r.then_branch(), complement != r.is_complement()));
+        as_expr(
+          r.then_branch(), complement != r.then_branch().is_complement()));
     }
   }
   else if(r.then_branch().is_constant())

Original file line number	Diff line number	Diff line change
`@@ -119,11 +119,14 @@ exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const`
`119`	`119`	`if(r.else_branch().is_complement() != complement)`
`120`	`120`	`{`
`121`	`121`	`return and_exprt(`
`122`		`- n_expr, as_expr(r.then_branch(), complement != r.is_complement()));`
	`122`	`+ n_expr,`
	`123`	`+ as_expr(`
	`124`	`+ r.then_branch(), complement != r.then_branch().is_complement()));`
`123`	`125`	`}`
`124`	`126`	`return or_exprt(`
`125`	`127`	`not_exprt(n_expr),`
`126`		`- as_expr(r.then_branch(), complement != r.is_complement()));`
	`128`	`+ as_expr(`
	`129`	`+ r.then_branch(), complement != r.then_branch().is_complement()));`
`127`	`130`	`}`
`128`	`131`	`}`
`129`	`132`	`else if(r.then_branch().is_constant())`