about summary refs log tree commit diff homepage
path: root/test/Solver/AShr_to_smtlib.kquery.good.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/Solver/AShr_to_smtlib.kquery.good.smt2')
-rw-r--r--test/Solver/AShr_to_smtlib.kquery.good.smt27
1 files changed, 7 insertions, 0 deletions
diff --git a/test/Solver/AShr_to_smtlib.kquery.good.smt2 b/test/Solver/AShr_to_smtlib.kquery.good.smt2
new file mode 100644
index 00000000..e9478da6
--- /dev/null
+++ b/test/Solver/AShr_to_smtlib.kquery.good.smt2
@@ -0,0 +1,7 @@
+;SMTLIBv2 Query 0
+(set-logic QF_AUFBV )
+(declare-fun shift () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun value () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(assert (and  (=  false (=  (_ bv0 8) (ite (bvuge (select  shift (_ bv0 32) ) (_ bv8 8) ) (_ bv0 8) (bvashr (select  value (_ bv0 32) ) (select  shift (_ bv0 32) ) ) ) ) ) (bvule  (_ bv8 8) (select  shift (_ bv0 32) ) ) ) )
+(check-sat)
+(exit)