---
source: tests/btor2_test.rs
expression: sys.serialize_to_str(&ctx)
---
Quiz1
input reset : bv<1>
bad %18 : bv<1> = not(implies(not(reset), not(ugt(counter, zext(4'b1010, 12)))))
node %15 : bv<1> = ugte(_resetCount, 1'b1)
node %16 : bv<1> = not(%15)
constraint %19 : bv<1> = implies(%16, reset)
state counter : bv<16>
  [next] ite(reset, 16'x0, add(zext(counter, 1), zext(1'b1, 16))[15:0])
state _resetCount : bv<1>
  [init] 1'b0
  [next] ite(%16, add(zext(_resetCount, 1), zext(1'b1, 1))[0], _resetCount)