obtain a random value
Major Section:  ACL2-BUILT-INS

(random$ 10 state) ==> (mv 7 <state>)

(Random$ limit state), where limit is a positive integer, returns a random non-negative integer together with a new state. Logically, it simply returns the first element of a list that is a field of the ACL2 state, called the acl2-oracle, together with the new state resulting from removing that element from that list. (Except, if that element is not in range as specified above, then 0 is returned.) However, random$ actually invokes a Common Lisp function to choose the integer returned. Quoting from the Common Lisp HyperSpec(TM), http://www.lispworks.com/documentation/HyperSpec/Front: ``An approximately uniform choice distribution is used... each of the possible results occurs with (approximate) probability 1/limit.''

Consider enabling rules natp-random$ and random$-linear if you want to reason about random$.