berkeley-abc/abc

BUG 'write_cex' get wrong answer

lanxuan365 opened this issue · 0 comments

For this aiger:

aag 8 0 4 1 4
2 4 2
4 2 4
6 8 6
8 6 8
16
10 7 3
12 6 2
14 13 11
16 14 1

// Use aigtoaig trans the aig to aag

I ran these cmds:
abc -c "read test.aig; logic; undc; strash; zero; bmc; cexsave; read test.aig; cexload; undc -c; testcex -a; write_cex -a /dev/stdout"
I got these:

Warning: The new network has no primary inputs. It is recommended
to add a dummy PI to make sure all commands work correctly.
The number of converted latches with DC values = 4.
Output 0 of miter "test" was asserted in frame 0. Time =     0.01 sec
Warning: The new network has no primary inputs. It is recommended
to add a dummy PI to make sure all commands work correctly.
Main AIG: The cex is correct.
1111# DONE

I trans the witness to the aiger witness format like this

1
b0
1111
.

But this witness cannot pass the aigsim.

I also got the dump aig by write_aiger:
abc -c "read test.aig; logic; undc; strash; zero; bmc; write_aiger dump.aig; write_cex -a /dev/stdout;"

1
b0
00000
1000
.

and the witness can pass the aigsim.

I check the 'testcex', I found the latch value in pAbc->Cex is correct(so undc -c is fine), but write_cex give the worng number.