Mercurial
Mercurial
>
repos
>
isabelle
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-6
+6
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Sun, 07 Nov 2010 17:56:07 +0100
blanchet
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
changeset
|
files
Sun, 07 Nov 2010 17:51:25 +0100
blanchet
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
changeset
|
files
Sun, 07 Nov 2010 13:29:59 +0100
blanchet
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
changeset
|
files
Sat, 06 Nov 2010 10:25:08 +0100
blanchet
make Nitpick datatype tests faster to make timeout less likely
changeset
|
files
Sat, 06 Nov 2010 10:25:08 +0100
blanchet
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
changeset
|
files
Sat, 06 Nov 2010 10:25:08 +0100
blanchet
always honor the max relevant constraint
changeset
|
files
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
-6
+6
+10
+30
+100
+300
+1000
+3000
+10000
+30000
tip