sat: dff output changes without clock edge

[widlarizer]

Version

main

On which OS did this happen?

Linux

Reproduction Steps

read_verilog -sv -icells <<EOT
module top(input C, D, output Q);
$_DFF_P_ ff (.C(C), .D(D), .Q(Q));
assume property (~C);
assert property (Q !== 1'bx);
endmodule
EOT
stat
chformal -lower
stat
sat -show-all -enable_undef -set-assumes -set-init-def -verify -prove-asserts -seq 2

Found when fixing tests/techmap/dfflibmap_formal.ys

Expected Behavior

QED

Actual Behavior

When D goes from def to undef, Q goes from def to undef, despite C not changing.

  Time Signal Name                             Dec       Hex           Bin
  ---- ------------------------------- ----------- --------- -------------
  init \Q                                        0         0             0
  ---- ------------------------------- ----------- --------- -------------
     1 $auto$rtlil.cc:3337:Not$12                0         0             0
     1 $auto$rtlil.cc:3337:Not$7                 0         0             0
     1 $auto$rtlil.cc:3384:And$14                0         0             0
     1 $auto$rtlil.cc:3384:And$9                 0         0             0
     1 $nex$<<EOT:4$4_Y                          1         1             1
     1 $not$<<EOT:3$2_Y                          1         1             1
     1 \C                                        0         0             0
     1 \D                                       --        --             x
     1 \Q                                        0         0             0
  ---- ------------------------------- ----------- --------- -------------
     2 $auto$rtlil.cc:3337:Not$12                0         0             0
     2 $auto$rtlil.cc:3337:Not$7                 1         1             1
     2 $auto$rtlil.cc:3384:And$14                0         0             0
     2 $auto$rtlil.cc:3384:And$9                 1         1             1
     2 $nex$<<EOT:4$4_Y                          0         0             0
     2 $not$<<EOT:3$2_Y                          1         1             1
     2 \C                                        0         0             0
     2 \D                                        0         0             0
     2 \Q                                       --        --             x

[widlarizer]

Without modeling undef, DFF's output can spontaneously update without a clock edge:

read_verilog -sv -icells <<EOT
module top(input C, D, output Q);
$_DFF_P_ ff (.C(C), .D(D), .Q(Q));
assume property (~C);
assert property (Q !== 1'b1);
endmodule
EOT
chformal -lower
sat -show-ports -set-init-zero -set-assumes -verify -prove-asserts -seq 2

  Time Signal Name             Dec
  ---- --------------- -----------
  init \Q                        0
  ---- --------------- -----------
     1 \C                        0
     1 \D                        1
     1 \Q                        0
  ---- --------------- -----------
     2 \C                        0
     2 \D                        0
     2 \Q                        1