csb produces incorrect model results #12
Description
For anything other than the most trivial inputs, csb's model results seem completely wrong.
Example input file:
(set-logic QF_BV)
(declare-const a (_ BitVec 6))
(declare-const b (_ BitVec 6))
(declare-projvar a b)
(assert (bvult #b000001 a))
(assert (bvult #b000001 b))
(assert (= (bvxor a b) #b000010))
(check-sat)
When I run csb:
$ ./csb -u -n 1 myproblem2.smt2
c [stp] using unigen backend
c Projection SMT variables: 2 Other variables: 0
c Sol count: 15*2**0
sat
(model
( define-fun |a| () (_ BitVec 6) #b001111 )
( define-fun |b| () (_ BitVec 6) #b000000 )
)
b is not larger than 1. And their XOR is also not 2.