; 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 reg0 : bv<8>
; [init] 8'b0
; [next] 8'b1
; state reg1 : bv<8>
; [init] 8'b0
; [next] reg0
1 sort bitvec 8 ; bv<8>
2 zero 1 ; 8-bit zero
3 one 1 ; 8-bit one
10 state 1 reg0
11 init 1 10 2 ; [init] 0
12 next 1 10 3 ; [next] 1
20 state 1 reg1
21 init 1 20 2 ; [init] 0
22 next 1 20 10 ; [next] reg0
; we expect to see the following execution:
; reg0 = 0 reg1 = 0
; reg0 = 1 reg1 = 0
; reg0 = 1 reg1 = 1