diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-13 03:35:48 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-13 03:35:48 +0000 |
commit | a412a17b48402372cc4208df04c3d80ecd5a1545 (patch) | |
tree | 9f8c2128d30b035c06b4697528e207725167f624 /test/regress/regress0/aufbv/fuzz05.delta01.smt | |
parent | 727d27b821805ec1b53c99815d7e33d8ea53d307 (diff) |
r2.node == response.node failure
Diffstat (limited to 'test/regress/regress0/aufbv/fuzz05.delta01.smt')
-rw-r--r-- | test/regress/regress0/aufbv/fuzz05.delta01.smt | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/fuzz05.delta01.smt b/test/regress/regress0/aufbv/fuzz05.delta01.smt new file mode 100644 index 000000000..b2dfdceff --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz05.delta01.smt @@ -0,0 +1,14 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((a2 Array[12:9])) +:status sast +:formula +(let (?n1 bv0[13]) +(let (?n2 (bvsdiv ?n1 ?n1)) +(let (?n3 bv0[12]) +(let (?n4 (select a2 ?n3)) +(let (?n5 (sign_extend[4] ?n4)) +(let (?n6 (bvmul ?n2 ?n5)) +(flet ($n7 (bvsge ?n1 ?n6)) +$n7 +)))))))) |