diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 02:32:04 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-11 02:32:04 +0000 |
commit | 15396a6a276baac5773905651f3fb66c3b675919 (patch) | |
tree | 71e661158aa9333bb2c2e6e6da0ec29e450441ee /test/regress/regress0/aufbv/fuzz01.delta01.smt | |
parent | c2bee2773194c51a67270535b475870d31b756c7 (diff) |
some failing examples
Diffstat (limited to 'test/regress/regress0/aufbv/fuzz01.delta01.smt')
-rw-r--r-- | test/regress/regress0/aufbv/fuzz01.delta01.smt | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/fuzz01.delta01.smt b/test/regress/regress0/aufbv/fuzz01.delta01.smt new file mode 100644 index 000000000..93ba564a3 --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz01.delta01.smt @@ -0,0 +1,25 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((v1 BitVec[3])) +:extrafuns ((v2 BitVec[11])) +:extrafuns ((a9 Array[8:5])) +:extrafuns ((a6 Array[1:13])) +:status unknown +:formula +(let (?n1 bv0[15]) +(let (?n2 bv0[1]) +(let (?n3 (zero_extend[8] v1)) +(let (?n4 (bvnor v2 ?n3)) +(let (?n5 (extract[7:0] ?n4)) +(let (?n6 bv0[5]) +(let (?n7 (store a9 ?n5 ?n6)) +(let (?n8 bv0[8]) +(let (?n9 (select ?n7 ?n8)) +(let (?n10 (zero_extend[8] ?n9)) +(let (?n11 (store a6 ?n2 ?n10)) +(let (?n12 (extract[0:0] ?n4)) +(let (?n13 (select ?n11 ?n12)) +(let (?n14 (zero_extend[2] ?n13)) +(flet ($n15 (= ?n1 ?n14)) +$n15 +)))))))))))))))) |