Sample Interpretation.

[lahiri-phdworks]

Thanks for the sampler tool.
I had one query regarding the sample produced.
How do I interpret the sample? I wanted to know the value of each bit vector entry corresponding to the variables I have.

; benchmark generated from python API
(set-info :smt-lib-version 2.6)
(set-logic QF_AUFBV)

(declare-fun x1 () (_ BitVec 32))
(declare-fun x2 () (_ BitVec 32))
(declare-fun a1 () (_ BitVec 32))
(declare-fun y1 () (_ BitVec 32))
(declare-fun y2 () (_ BitVec 32))
(declare-fun n2 () (_ BitVec 32))
(declare-fun n1 () (_ BitVec 32))
(declare-fun a2 () (_ BitVec 32))
;; Loop body operations
(assert
 (= x2 (bvadd x1 (_ bv1 32))))
(assert
 (= y2 (bvadd y1 a1)))
;; Transfer across the loop body.
(assert
 (= n1 n2))
(assert
 (= a1 a2))
 ;; Inv(x1, y1, n1, a1) && (x1 <= n1) => Inv(x2, y2, n2, a2)
(assert
 (let (($x49 (and (= y2 (bvmul x2 a2)) (bvsle x2 n2))))
 (let (($x45 (and (and (= y1 (bvmul x1 a1)) (bvsle x1 n1)) (bvslt x1 n1))))
 (=> $x45 $x49))))
 ;; DataSet Constraints
 ;; n > 0, y != 0, x != 0, a > 0
(assert
 (bvsgt n1 (_ bv0 32)))
(assert
 (bvsgt a1 (_ bv0 32)))
(assert
 (and (distinct y1 (_ bv0 32)) true))
(assert
 (and (distinct x1 (_ bv0 32)) true))

(check-sat)
(exit)

This is the file and samples are

999ea4ca�999ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4c9�999ea4c8�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ce�999ea4cd�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4c2�999ea4c1�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4da�999ea4d9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ea�999ea4e9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea48a�999ea489�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea44a�999ea449�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea5ca�999ea5c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea6ca�999ea6c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea0ca�999ea0c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999eacca�999eacc9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999eb4ca�999eb4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999e84ca�999e84c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ee4ca�999ee4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999e24ca�999e24c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999fa4ca�999fa4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ca4ca�999ca4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999aa4ca�999aa4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
9996a4ca�9996a4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
998ea4ca�998ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
99bea4ca�99bea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
99dea4ca�99dea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
991ea4ca�991ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
989ea4ca�989ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
9b9ea4ca�9b9ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
9d9ea4ca�9d9ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
919ea4ca�919ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
899ea4ca�899ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
b99ea4ca�b99ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
d99ea4ca�d99ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
199ea4ca�199ea4c9�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4cc�999ea4cb�6c1f10c2�40466e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10c3�40466e41�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10c0�40466e40�2bd8a280�4e44df19�4e44df19�2bd8a280�
999ea4ca�999ea4c9�6c1f10c6�40466e44�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10ca�40466e48�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10d2�40466e50�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f10e2�40466e60�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f1082�40466e00�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f1142�40466ec0�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f11c2�40466f40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f12c2�40466c40�2bd8a682�4e44df19�4e44df19�2bd8a682�
999ea4ca�999ea4c9�6c1f14c2�40466e40�2bd8a682�4e44df19�4e44df19�2bd8a682�
999ea4ca�999ea4c9�6c1f08c2�40466640�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f20c2�40467e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f50c2�4046ae40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1f90c2�4046ee40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1e10c2�40456e40�2bd8a282�4e44df19�4e44df19�2bd8a282�
999ea4ca�999ea4c9�6c1d10c2�40446e40�2bd8a282�4e44df19�4e44df19�2bd8a282�

[Shangyint]

I am having the same issure here. I assume the bits occured the same order as your query defines them. It would be great if this can be confirmed by the author.

Also btw may I ask which API method did you use to generate this SMT-LIB format query? I am using solver.sexpr() and it doesn't come with the correct logic theory. Thanks!