CSB 2.0.3 introduces non-determinism and illegal solutions

[terpstra]

I think your fix for unconstrained variables in 2.0.3 has introduced new bugs.

It now has non-deterministically incorrect output on "normal" problems:

$ cat problem.1.smt
(set-logic QF_BV)
(declare-const Z.cond1 Bool)
(declare-const Z.cond2 Bool)
(declare-const Z.a (_ BitVec 2))
(declare-const Z.b (_ BitVec 2))
(declare-const Z.c (_ BitVec 2))
(declare-const Z.result (_ BitVec 32))
(assert 
  (and 
    (and 
      (and true (= Z.result (concat (concat #b00 #x0000000) (ite Z.cond1 Z.a (ite Z.cond2 Z.b Z.c))))) 
      (not (= ((_ extract 1 1) Z.a) #b1))) 
    (and (not (= ((_ extract 1 1) Z.b) #b1)) (not (= ((_ extract 1 1) Z.c) #b1)))))
(check-sat)
$ csb -n1 -s  --seed 12 problem.1.smt2
c [stp] using cmsgen backend
c No variables declared as projection var, moving to non-projection mode
c Projection SMT variables: 6 Other variables: 0
sat
(model
( define-fun |Z.cond1| () Bool true ) ; <--- This value toggles randomly between true/false when rerun
( define-fun |Z.cond2| () Bool true )
( define-fun |Z.a| () (_ BitVec 2) #b00 )
( define-fun |Z.b| () (_ BitVec 2) #b01 )
( define-fun |Z.c| () (_ BitVec 2) #b00 )
( define-fun |Z.result| () (_ BitVec 32) #x00000001 )
)

When Z.cond1 is true, result must be 0. So csb is producing non-deterministic output, and sometimes that output is wrong.

[terpstra]

This example always produces the same (correct) answer with 2.0.1