blob: 774c46d9a7f828da836092fd1f5534ca21b2bf32 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
# RUN: %kleaver -print-smtlib -smtlib-abbreviation-mode=none %s > %t
# RUN: diff -u %t %s.good.smt2
# This test tries to check that the SMT-LIBv2 we generate when a AShrExpr is
# used is correct.
#
# FIXME: We should really pass the generated query to an SMT solver that supports
# SMT-LIBv2 and check it gives the correct answer ``unsat``. An older version of
# KLEE where AShrExpr wasn't handled correctly would give ``sat`` for this query.
#
# We could fix this if we required STP to be in the user's PATH and made available
# as a substitution in llvm-lit
array value[1] : w32 -> w8 = symbolic
array shift[1] : w32 -> w8 = symbolic
(query [(Ule 8 (Read w8 0 shift))] (Eq 0 (AShr w8 (Read w8 0 value) (Read w8 0 shift))) )
|
