diff options
Diffstat (limited to 'test/regress/regress0/uf/ccredesign-fuzz.smt')
-rw-r--r-- | test/regress/regress0/uf/ccredesign-fuzz.smt | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/test/regress/regress0/uf/ccredesign-fuzz.smt b/test/regress/regress0/uf/ccredesign-fuzz.smt deleted file mode 100644 index d7a658600..000000000 --- a/test/regress/regress0/uf/ccredesign-fuzz.smt +++ /dev/null @@ -1,32 +0,0 @@ -(benchmark fuzzsmt -:logic QF_UF -:status sat -:extrasorts (S1) -:extrasorts (S0) -:extrafuns ((v0 S0)) -:extrafuns ((v1 S0)) -:extrafuns ((f4 S1 S1)) -:extrafuns ((v2 S1)) -:extrafuns ((v3 S1)) -:extrapreds ((p3 S0 S0 S1)) -:extrafuns ((f0 S0 S0 S1 S0)) -:extrapreds ((p1 S0 S1 S1)) -:extrapreds ((p4 S1)) -:formula -(flet ($n1 (p4 v3)) -(let (?n2 (f4 v2)) -(flet ($n3 (p4 ?n2)) -(flet ($n4 (p1 v0 ?n2 ?n2)) -(let (?n5 (f0 v1 v1 v2)) -(let (?n6 (ite $n4 ?n5 v0)) -(flet ($n7 (p3 ?n6 v0 ?n2)) -(flet ($n8 (iff $n3 $n7)) -(flet ($n9 (= v3 ?n2)) -(let (?n10 (ite $n9 v1 v0)) -(flet ($n11 (distinct ?n10 ?n10)) -(flet ($n12 false) -(flet ($n13 (implies $n11 $n12)) -(flet ($n14 (implies $n13 $n12)) -(flet ($n15 (if_then_else $n1 $n8 $n14)) -$n15 -)))))))))))))))) |