mvsis> simplify -t 1000
red_adder:  3 nodes,  3 POs,  315 cubes(sop),  2010 lits(sop),  156 lits(fact.)
mvsis>
mvsis> simplify -t 1000 -m exact
red_adder:  3 nodes,  3 POs,  300 cubes(sop),  1989 lits(sop),  130 lits(fact.)
mvsis>
mvsis> validate -m mdd red-add-bin.mv
Networks differ on (at least) primary output s1 i-set 0
Incorrect input is:
0 x1_b0
1 x1_b1
1 x1_b2
0 x0_b0
0 x0_b1
0 x0_b2
0 y1_b0
0 y1_b1
0 y1_b2
0 y0_b0
0 y0_b1
0 y0_b2
0 cin_b0
0 cin_b1
0 cin_b2
Networks are NOT combinationally equivalent.
red_adder:  3 nodes,  3 POs,  300 cubes(sop),  1989 lits(sop),  130 lits(fact.)
mvsis>