1 files changed, 39 insertions, 0 deletions
diff --git a/src/lfsc/tests/vmcai_bytes.smt2 b/src/lfsc/tests/vmcai_bytes.smt2
new file mode 100644
index 0000000..6628e37
--- /dev/null
+++ b/src/lfsc/tests/vmcai_bytes.smt2
@@ -0,0 +1,39 @@
+(set-logic QF_ABV)
+(declare-fun initialMemoryState_0x2ae2bf0 () (Array (_ BitVec 64) (_ BitVec 8)))
+(assert
+(let ((x1 (_ bv1 8)))
+(let ((x2 (_ bv0 32)))
+(let ((x3 (_ bv3221225470 64)))
+(let ((x4 (_ bv3221225468 64)))
+(let ((x5 initialMemoryState_0x2ae2bf0))
+(let ((x6 (_ bv3221225468 64)))
+(let ((x7 ((_ extract 7 0) x2)))
+(let ((x8 (store x5 x6 x7)))
+(let ((x9 (_ bv3221225469 64)))
+(let ((x10 ((_ extract 15 8) x2)))
+(let ((x11 (store x8 x9 x10)))
+(let ((x12 (_ bv3221225470 64)))
+(let ((x13 ((_ extract 23 16) x2)))
+(let ((x14 (store x11 x12 x13)))
+(let ((x15 (_ bv3221225471 64)))
+(let ((x16 ((_ extract 31 24) x2)))
+(let ((x17 (store x14 x15 x16)))
+(let ((x18 (store x17 x3 x1)))
+(let ((x19 (_ bv3221225468 64)))
+(let ((x20 (select x18 x19)))
+(let ((x21 (_ bv3221225469 64)))
+(let ((x22 (select x18 x21)))
+(let ((x23 (_ bv3221225470 64)))
+(let ((x24 (select x18 x23)))
+(let ((x25 (_ bv3221225471 64)))
+(let ((x26 (select x18 x25)))
+(let ((x27 (concat x22 x20)))
+(let ((x28 (concat x24 x27)))
+(let ((x29 (concat x26 x28)))
+(let ((dollar_x30 (not (=  x29 x2))))
+(let ((dollar_x31 (not dollar_x30)))
+dollar_x31
+)))))))))))))))))))))))))))))))
+)
+(check-sat)
+(exit)