diff options
Diffstat (limited to 'test/regress/regress0/aufbv')
-rw-r--r-- | test/regress/regress0/aufbv/Makefile.am | 9 | ||||
-rw-r--r-- | test/regress/regress0/aufbv/rewrite_bug.smt | 28 |
2 files changed, 32 insertions, 5 deletions
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 41bb5db5b..482c06ac7 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -22,9 +22,10 @@ TESTS = \ wchains010ue.delta02.smt \ dubreva005ue.delta01.smt \ fuzz00.smt \ + fuzz01.smt \ fuzz01.delta01.smt \ fuzz02.delta01.smt \ - fuzz02.smt \ + fuzz02.smt \ fuzz03.delta01.smt \ fuzz03.smt \ fuzz04.delta01.smt \ @@ -37,11 +38,9 @@ TESTS = \ fuzz08.smt \ fuzz09.smt \ fuzz10.smt \ - fifo32bc06k08.delta01.smt + fifo32bc06k08.delta01.smt \ + rewrite_bug.smt -# failing -# fuzz01.smt \ -# EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/aufbv/rewrite_bug.smt b/test/regress/regress0/aufbv/rewrite_bug.smt new file mode 100644 index 000000000..c0906ba0d --- /dev/null +++ b/test/regress/regress0/aufbv/rewrite_bug.smt @@ -0,0 +1,28 @@ +(benchmark B_ +:logic QF_AUFBV +:extrafuns ((a Array[32:8])) +:status sat +:formula +(flet ($n1 true) +(let (?n2 bv0[8]) +(let (?n3 (sign_extend[24] ?n2)) +(let (?n4 bv1[32]) +(let (?n5 bv1[8]) +(let (?n6 (store a ?n4 ?n5)) +(let (?n7 bv0[32]) +(let (?n8 (select a ?n4)) +(let (?n9 (sign_extend[24] ?n8)) +(let (?n10 (extract[7:0] ?n9)) +(let (?n11 (store ?n6 ?n7 ?n10)) +(let (?n12 (select ?n11 ?n4)) +(let (?n13 (store ?n11 ?n4 ?n12)) +(let (?n14 (select ?n13 ?n7)) +(let (?n15 (sign_extend[24] ?n14)) +(flet ($n16 (bvslt ?n3 ?n15)) +(flet ($n17 (not $n16)) +(let (?n18 (select ?n13 ?n4)) +(let (?n19 (sign_extend[24] ?n18)) +(flet ($n20 (bvslt ?n7 ?n19)) +(flet ($n21 (and $n1 $n1 $n1 $n1 $n17 $n20)) +$n21 +)))))))))))))))))))))) |