diff options
Diffstat (limited to 'test/regress/regress0/auflia/x2.smt')
-rw-r--r-- | test/regress/regress0/auflia/x2.smt | 28 |
1 files changed, 0 insertions, 28 deletions
diff --git a/test/regress/regress0/auflia/x2.smt b/test/regress/regress0/auflia/x2.smt deleted file mode 100644 index 3566d9858..000000000 --- a/test/regress/regress0/auflia/x2.smt +++ /dev/null @@ -1,28 +0,0 @@ -(benchmark fuzzsmt -:logic QF_AUFLIA -:extrafuns ((v4 Array)) -:extrafuns ((f0 Int Int)) -:extrapreds ((p0 Int Int Int)) -:status sat -:formula -(let (?n1 0) -(flet ($n2 (p0 ?n1 ?n1 ?n1)) -(let (?n3 1) -(let (?n4 (ite $n2 ?n3 ?n1)) -(flet ($n5 (< ?n1 ?n4)) -(flet ($n6 (p0 ?n3 ?n1 ?n1)) -(let (?n7 (ite $n6 ?n3 ?n1)) -(let (?n8 (ite $n5 ?n7 ?n3)) -(flet ($n9 (< ?n1 ?n8)) -(flet ($n10 true) -(let (?n11 3) -(let (?n12 (f0 ?n1)) -(let (?n13 (* ?n11 ?n12)) -(let (?n14 (select v4 ?n1)) -(flet ($n15 (> ?n13 ?n14)) -(flet ($n16 (xor $n10 $n15)) -(flet ($n17 false) -(flet ($n18 (implies $n16 $n17)) -(flet ($n19 (and $n9 $n18)) -$n19 -)))))))))))))))))))) |