Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
repaired logic for default provers -- ensures Z3 is kept if installed and configured as noncommercial
|
file |
diff |
annotate
|
Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file |
diff |
annotate
|
Thu, 06 Feb 2014 01:13:44 +0100 |
blanchet |
try right bunch of methods
|
file |
diff |
annotate
|
Tue, 04 Feb 2014 23:11:18 +0100 |
blanchet |
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 23:38:33 +0100 |
blanchet |
properly overwrite replay data from one compression iteration to another
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 17:13:31 +0100 |
blanchet |
added 'smt' option to control generation of 'by smt' proofs
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 16:53:58 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 15:19:07 +0100 |
blanchet |
merged 'reconstructors' and 'proof methods'
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 16:07:20 +0100 |
blanchet |
moved ML code around
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 13:42:47 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 13:32:13 +0100 |
blanchet |
guarded against exception
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 12:30:54 +0100 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
| base
|