; Copyright 2023 The Regents of the University of California
; released under BSD 3-Clause License
; author: Kevin Laeufer <laeufer@berkeley.edu>
;
; This tests for a bug in updating next states. The system looks like this:
; state a : bv<8>
;   [init] 8'b0
;   [next] b
; state b : bv<8>
;   [init] 8'b1
;   [next] a

1 sort bitvec 8 ; bv<8>
2 zero 1        ; 8-bit zero
3 one  1        ; 8-bit one

10 state 1 a
11 init 1 10 2  ; [init] 0

20 state 1 b
21 init 1 20 3  ; [init] 1
22 next 1 20 10 ; [next] a

12 next 1 10 20 ; [next] b