[alt-ergo/f13/master] Update to version 0.92.1
David A. Wheeler
dwheeler at fedoraproject.org
Sat Oct 9 15:43:46 UTC 2010
commit aee27769b6259b418fe8684ceaa3f66f9aca5337
Author: David A. Wheeler <dwheeler at dwheeler.com>
Date: Sat Oct 9 11:43:52 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
More information about the scm-commits
mailing list