A strange bug

[Huangps]

The attached archive contains four .sm2 files with the following SMT solving results:
test1 -- Solving (assert (and (or A B))) yields unsat.
test2 -- Solving (assert (and (or A))) yields sat.
test3 -- Solving (assert (and (or B))) yields sat.
test4 -- Solving (assert (and (or B A))) yields sat.

test1.txt
test2.txt
test3.txt
test4.txt