1 files changed, 28 insertions, 0 deletions
diff --git a/src/lfsc/tests/bv_artih.smt2 b/src/lfsc/tests/bv_artih.smt2
new file mode 100644
index 0000000..a6db769
--- /dev/null
+++ b/src/lfsc/tests/bv_artih.smt2
@@ -0,0 +1,28 @@
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
+(declare-fun c () (_ BitVec 4))
+(declare-fun d () (_ BitVec 4))
+
+;; (assert (= a #b0010))
+;; (assert (= b #b0110))
+;; (assert (= c #b1000))
+;; (assert (= d #b0010))
+
+(assert (= #b0010 a))
+(assert (= #b0110 b))
+(assert (= #b1000 c))
+(assert (= #b0010 d))
+
+;; (assert (= #b1111 a))
+;; (assert (= #b1111 b))
+;; (assert (= #b1111 c))
+;; (assert (= #b1111 d))
+
+(assert
+ (not (= (bvand (bvand a b) d) d)))
+
+;; (assert
+;;  (not (= (bvadd a b) (bvadd b (bvadd a #b1111)))))
+(check-sat)
+(exit)