- 21 Jun, 2017 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 18 Jun, 2017 2 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 16 Jun, 2017 1 commit
-
-
MARCHE Claude authored
-
- 13 Jun, 2017 1 commit
-
-
Johannes Kanig authored
On N127-001, an optimisation of the fast WP was introduced, based on marking states that contain variables that need to be refreshed when merging them. However, this "marked" status was incorrectly reset to false when merging states, even though some of those "unfresh" variables could survive the merge. The consequence was that the WP was reusing variables too aggressively, which would result in incorrect VCs. We now compute the marked status of a merged state from the states to be merged: if one of them is marked, the merged state is marked too. mlw_wp.ml: (merge): synthetize marked status from input states Change-Id: Ifb02c54fca58137c31762469e48b59e7c907b995
-
- 12 Jun, 2017 6 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
- most important improvement : the explanation, used as first part of the shape was computed twice ! (at least) - several improvements in the implementation, avoid using Format in particular (done also in checksum computations) - possible further improvements: do not compute shapes if checksums are OK (they must be the same as in previous session) do not compute goal checksums if theory checksum is OK (they must be the same as in previous session)
-
- 08 Jun, 2017 1 commit
-
-
MARCHE Claude authored
-
- 24 May, 2017 1 commit
-
-
MARCHE Claude authored
If drivers in why3.conf are simple names like "alt_ergo", then the driver file is search as <datadir>/drivers/alt_ergo.drv This behavior is now the same as when a driver is given with option -D on the command line for why3prove, why3replay or why3extract Reminder: the datadir is either given as 1) the environment variable WHY3DATA 2) the field "datadir" of the [main] section of the why3 config file if exists 3) or by default the compile-time datadir
-
- 22 May, 2017 1 commit
-
-
MARCHE Claude authored
The underlying Monoid does not need to be commutative, and is indeed not in example fibonacci.mlw
-
- 19 May, 2017 3 commits
-
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
- 16 May, 2017 1 commit
-
-
MARCHE Claude authored
-
- 15 May, 2017 1 commit
-
-
Guillaume Melquiond authored
-
- 12 May, 2017 1 commit
-
-
MARCHE Claude authored
-
- 10 May, 2017 2 commits
-
-
MARCHE Claude authored
-
François Bobot authored
-
- 05 May, 2017 1 commit
-
-
Mário Pereira authored
-
- 27 Apr, 2017 1 commit
-
-
Martin Clochard authored
-
- 20 Apr, 2017 3 commits
-
-
Jean-Christophe Filliâtre authored
(so that we can use it with 'why3 execute')
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
- 19 Apr, 2017 1 commit
-
-
Jean-Christophe Filliâtre authored
-
- 13 Apr, 2017 2 commits
-
-
Guillaume Melquiond authored
-
Guillaume Melquiond authored
-
- 12 Apr, 2017 8 commits
-
-
MARCHE Claude authored
-
Sylvain Dailler authored
-
Johannes Kanig authored
For every check, we now print the "check_tree" into the JSON output. This is basically a dump of the session tree, just in a different format. * json.ml new json datatype and new function "print_json" to print it Change-Id: I0b28ac181793af4d160abc58c2634b3cbcac9b94
-
Sylvain Dailler authored
Parsing reference was forgotten in commit for Q217-025. This solves the problem with a new token MK_ANYTHING. * src/driver/parse_smtv2_model_lexer.mll (parse): Added lexing for all remaining mk*___ record constructs. * src/driver/parse_smtv2_model_parser.mly (smt_term): An smt_term can be a reference to a smt_term. It means it can be (Mk_anything smt_term). Change-Id: Ib529fee83d16d09266e526ca5fb3c65526addff5
-
Sylvain Dailler authored
Added a counter for constructors. We print a new functions to redefine constructors only if there is a need. * src/printer/smtv2_cvc_ce.ml (print_constructor_decl): Added counter. (print_data_decl): Added counter. (print_saved_constructors): Print only if number of constructors in the list is greater than counter. Change-Id: Iad0f29caac961644dcbf4137341abd76c01e1090
-
Sylvain Dailler authored
Do not print (get-info :reason-unknown) on smt2 output. Previously, detection of end of model and beginning of statistics was done by using the reason. We now detect a single parenthesis on a line: every cvc4 model ends with this (we assume statistics does not contain a line beginning with a closing parenthesis). As a side effect, we also find more counterexamples. * src/driver/parse_smtv2_model.ml (parse): Revert changes that were detecting Abort trap. * src/driver/parse_smtv2_model_parser.mly (output): Revert changes to allow absence of parenthesis at the end. Also removed parsing on results given by the reason. Now match on ). * src/printer/smtv2_cvc_ce.ml (print_prop_decl): Remove (get-info :reason-unknown). * src/printer/smtv2.ml (print_prop_decl): Remove get-info for coherence. Change-Id: Ifbd7b2b9ce499f8aaa020f58375d784793990965
-
Sylvain Dailler authored
This patch allows parsing model including the error message raised by cvc4 on mac. * src/driver/parse_smtv2_model.ml (parse): Allow parsing of specific error message "Abort trap". (output): Allow parsing when last parenthesis is missing which is the case when the bug is occuring. Change-Id: I80d7276d37916e09ba4bb28478ac9a7427789771
-
Sylvain Dailler authored
Change-Id: Id165717756375db150031589740470cc1e08b8ac
-