Bug in zeroing AIG

[sirandreww]

I'm running the following command ./abc -c "read "rast-p19.aig" ; zero ; fold2 ; pdr -v"
This is the output that I receive:

ABC command line: "read rast-p19.aig ; zero ; fold2 ; pdr -v".

Converting 18 flops from don't-care to zero initial value.
Warning: The network has no constraints.
VarMax = 300. FrameMax = 10000. QueMax = 0. TimeMax = 0. MonoCNF = no. SkipGen = no. SolveAll = no.
Frame Clauses                                                     Max Queue Flops Cex      Time
  1 : 0 1                                                                 1     1      0.10 sec
  2 : 0 0 1                                                               0     1      0.10 sec
Invariant F[1] : 1 clauses with 1 flops (out of 2602) (cex = 0, ave = 2.00)
Verification of invariant with 1 clauses was successful.  Time =     0.00 sec
Block =    1  Oblig =     1  Clause =     1  Call =     5 (sat=20.0%)  Cex =   0  Start =   0
SAT solving =     0.00 sec (  1.02 %)
  unsat     =     0.00 sec (  1.00 %)
  sat       =     0.00 sec (  0.02 %)
Generalize  =     0.00 sec (  0.51 %)
Push clause =     0.00 sec (  0.57 %)
Ternary sim =     0.00 sec (  0.02 %)
Containment =     0.00 sec (  0.00 %)
CNF compute =     0.00 sec (  0.11 %)
Refinement  =     0.00 sec (  0.00 %)
TOTAL       =     0.11 sec (100.00 %)
Property proved.  Time =     0.12 sec

As in this problem is UNSAT.

However, this rast-p19 is from HWMCC20 and is known to be SAT. More specifically it is known to be satisfied by an initial state. Thus I suspect there is an issue with zero.

[zhanghongce]

IMO, zero should not be used, because it converts 1-initialized and uninitialized latches to 0-initialized, which obviously changed the initial condition of the transition system.

[sirandreww]

Correct, I addressed this in #281