; (a = b) ^ (a = b & 00000) ^ (b = 11111) is UNSAT

(check
(% a var_bv
(% b var_bv
(% f1 (th_holds (= (BitVec 4) (a_var_bv _ a) (a_var_bv _ b)))
(% f2 (th_holds (= (BitVec 4) (a_var_bv _ a) (bvand 4 (a_var_bv 4 b) (a_bv _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn)))))))))
(% f3 (th_holds (= (BitVec 4) (a_var_bv _ b) (a_bv _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
(: (holds cln)

;; (decl_bv_term_var 5 a (\ ba1
;; (decl_bv_term_var 5 b (\ ba2
;; (decl_bv_term_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
;; (decl_bv_term_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4

(decl_atom (bitof a 4) (\ v1 (\ a1
(decl_atom (bitof b 4) (\ v2 (\ a2

; bitblasting terms
(decl_bblast _ _ _ (bv_bbl_var 4 a _ ) (\ bt1
(decl_bblast _ _ _ (bv_bbl_var 4 b _ ) (\ bt2
(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bt3
(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bt4
(decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5

; bitblasting formulas
(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt1 bt2) (\ bf1
(th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2
(th_let_pf _ (bv_bbl_= _ _ _ _ _ _ bt2 bt4) (\ bf3

; CNFication
; a.4 V ~b.4
(satlem _ _
(asf _ _ _ a1 (\ l1
(ast _ _ _ a2 (\ l2
(clausify_false
  trust
))))) (\ C2

; ~a.4
(satlem _ _
(ast _ _ _ a1 (\ l1
(clausify_false
  trust
))) (\ C3

; b.4
(satlem _ _
(asf _ _ _ a2 (\ l2
(clausify_false
  trust
))) (\ C6


(satlem_simplify _ _ _
(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))

)))))))))))))))))))))))))))))))))))))))))))))