[alt-ergo/f14/master] Update to version 0.92.1

[David A. Wheeler]

commit 14d1959b76e3ab12c8a7c264d14ea8feba6dbd47
Author: David A. Wheeler <dwheeler at dwheeler.com>
Date:   Sat Oct 9 11:15:20 2010 -0400

    Update to version 0.92.1

 .gitignore    |    1 +
 alt-ergo.spec |   27 ++++++++++++++++++++++-----
 sources       |    2 +-
 swap0_why.why |    2 --
 4 files changed, 24 insertions(+), 8 deletions(-)
---
diff --git a/.gitignore b/.gitignore
index fe72694..55bb8b4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 alt-ergo-0.9.tar.gz
+/alt-ergo-0.92.1.tar.gz
diff --git a/alt-ergo.spec b/alt-ergo.spec
index c0aaf72..871cffa 100644
--- a/alt-ergo.spec
+++ b/alt-ergo.spec
@@ -12,9 +12,9 @@
 %define __find_provides /usr/lib/rpm/ocaml-find-provides.sh
 
 Name:		alt-ergo
-Version:	0.9
-Release:	2%{?dist}
-Summary:	Alt-Ergo automatic theorem prover
+Version:	0.92.1
+Release:	1%{?dist}
+Summary:	Automated theorem prover including linear arithmetic
 
 Group:		Applications/Engineering
 License:	CeCILL-C
@@ -43,6 +43,10 @@ instantiation mechanism by which it fully supports quantifiers.
 
 cp -p %{SOURCE1} %{SOURCE2} .
 
+# Set print_flag to false or invoking with -select
+# from "why" will pause every invocation :-(.
+sed -i -e 's/let print_flag = true/let print_flag = false/;' pruning.ml
+
 %build
 # Avoid a Makefile patch by just adding this empty file, and thus autoconf
 # doesn't complain (better than ignoring all status from configure)
@@ -73,13 +77,13 @@ execstack -c ./alt-ergo.opt
 %else
 %define altergo ./alt-ergo.byte
 %endif
-%{altergo} swap0_why.why
+%{altergo} -arrays swap0_why.why
 
 %install
 rm -rf %{buildroot}
 
 mkdir -p %{buildroot}%{_bindir}
-make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir} MANDIR=%{buildroot}%{_mandir} install
+make %{opt_option} BINDIR=%{buildroot}%{_bindir} LIBDIR=%{buildroot}%{_datadir}/%{name} MANDIR=%{buildroot}%{_mandir} install
 
 %clean
 rm -rf %{buildroot}
@@ -92,6 +96,19 @@ rm -rf %{buildroot}
 %doc README.alt-ergo COPYING CeCILL-C CHANGES
 
 %changelog
+* Tue Oct 06 2010 David A. Wheeler <dwheeler at dwheeler.com> 0.92.1-1
+- Update to version 0.92.1. This means:
+- New built-in syntax for the theory of arrays
+- Fixes a bug in the arithmetic module
+- Allows folding and unfolding of predicate definitions
+
+* Tue Jun 08 2010 David A. Wheeler <dwheeler at dwheeler.com> 0.91-1
+- Update to version 0.91. This means:
+- partial support for non-linear arithmetics
+- support case split on integer variables
+- new support for Euclidean division and modulo operators
+
+
 * Tue Aug 04 2009 Alan Dunn <amdunn at gmail.com> 0.9-2
 - Added ExcludeArch sparc64 due to no OCaml
 
diff --git a/sources b/sources
index 023a205..2f67953 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-c7eb6d07391acdfa39bb00978105858d  alt-ergo-0.9.tar.gz
+4940caa641230c12c892262f91cb99b6  alt-ergo-0.92.1.tar.gz
diff --git a/swap0_why.why b/swap0_why.why
index 4727c77..fedaafe 100644
--- a/swap0_why.why
+++ b/swap0_why.why
@@ -163,8 +163,6 @@ logic real_min : real, real -> real
 
 predicate zwf_zero(a: int, b: int) = ((0 <= b) and (a < b))
 
-type 'a farray
-
 logic access : 'a1 farray, int -> 'a1
 
 logic update : 'a1 farray, int, 'a1 -> 'a1 farray