Parse Z3 counterexample into Python test case

[duouyang]

Hi there,

I am currently working on a project which needs to convert a Z3 counterexample into Python test cases. I am pretty new to Z3, so I am wondering is there a function or any resource that can help me do this.

Example
I got the following by using s.model
Store(K(BitVec(32), 1), 0, 10)
I would like to be [10, 1, 1, 1]

Thanks in advance!