[circt-bmc] `verif.assume` constraints on past timesteps are dropped by per-cycle pop

Since #7900, the BMC loop in VerifToSMT does smt.pop 1; smt.push 1 at the top of each iteration, discarding all assertions from the previous step. This correctly retracts the previous step's property-violation assert, but also discards verif.assume constraints, which must hold on the whole trace. A model at step n is then free to assign assumption-violating values to step n−1 inputs that feed registers, producing spurious counterexamples.

hw.module @AssumeDrop(in %clk: !seq.clock, in %in: i1) {
  %init = seq.initial () {
    %c1 = hw.constant true
    seq.yield %c1 : i1
  } : () -> !seq.immutable<i1>
  %r = seq.compreg %in, %clk initial %init : i1
  verif.assume %in : i1
  verif.assert %r : i1
}

circt-bmc repro.mlir -b 6 --module AssumeDrop --shared-libs=libz3.so reports "Assertion can be violated!"; hardwiring %in to 1 instead of assuming it reports no violations.

Disclosure: ran into this while vibecoding, take that however you want.