add test

yoni206 · Nov 23, 2023 · e0d54b8 · e0d54b8
1 parent 15a4bd7
commit e0d54b8
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/test/regress/cli/regress2/bv_to_int_issue_9053.smt2 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)