diff options
Diffstat (limited to 'test/regress/regress0/arrays/x2.smt')
| -rw-r--r-- | test/regress/regress0/arrays/x2.smt | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/test/regress/regress0/arrays/x2.smt b/test/regress/regress0/arrays/x2.smt deleted file mode 100644 index c043e88b9..000000000 --- a/test/regress/regress0/arrays/x2.smt +++ /dev/null @@ -1,17 +0,0 @@ -(benchmark read5.smt -:logic QF_AX -:status unsat -:extrafuns ((a Index)) -:extrafuns ((S Array)) -:extrafuns ((SS Array)) -:status unknown -:formula -(flet ($n1 (= S SS)) -(let (?n2 (select S a)) -(let (?n3 (store SS a ?n2)) -(flet ($n4 (= S ?n3)) -(flet ($n5 true) -(flet ($n6 (if_then_else $n1 $n4 $n5)) -(flet ($n7 (not $n6)) -$n7 -)))))))) |