diff --git a/test/regress/cli/regress2/bv_to_int_issue_9053.smt2 b/test/regress/cli/regress2/bv_to_int_issue_9053.smt2 new file mode 100644 index 00000000000..222c423a6fe --- /dev/null +++ b/test/regress/cli/regress2/bv_to_int_issue_9053.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --solve-bv-as=iand --check-models +; EXPECT: sat +(set-logic ALL) +(declare-fun a () (Array Int Int)) +(declare-fun b ((_ BitVec 3)) Int) +(declare-fun c () (_ BitVec 3)) +(declare-fun d () (_ BitVec 3)) +(assert (distinct (select a (b (bvand c d))) (select a (b (bvor c d))))) +(check-sat)