; we need QF_UFBV for this poof (set-logic QF_UFBV) ; insert the auto-generated code here %% ; declare two state variables s1 and s2 (declare-fun s1 () test_s) (declare-fun s2 () test_s) ; state s2 is the successor of state s1 (assert (test_t s1 s2)) ; we are looking for a model with y non-zero in s1 (assert (distinct (|test_n y| s1) #b0000)) ; we are looking for a model with y zero in s2 (assert (= (|test_n y| s2) #b0000)) ; is there such a model? (check-sat)