| Convert non-free record values to epsilon terms |
|
More...
|
over 4 years ago
|
| Add fields rsymbols to record values |
|
More...
|
over 4 years ago
|
| Expose only fields desc and ty for type value |
|
More...
|
over 4 years ago
|
| Format help text for why3 prove and execute |
|
More...
|
over 4 years ago
|
| Merge branch 'convert-exec-trace-to-ce-model' into 'master' |
|
More...
|
over 4 years ago
|
| Print anormal results from why3 execute to stderr |
|
More...
|
over 4 years ago
|
| Keep at most one empty model when checking counterexamples |
|
More...
|
over 4 years ago
|
| Track used definitions in task_of_term |
|
More...
|
over 4 years ago
|
| Store pmodule in Pinterp.env |
|
More...
|
over 4 years ago
|
| more examples from Rustan's book |
|
More...
|
over 4 years ago
|
| Merge branch 'allows-namespace-in-for-each' into 'master' |
|
More...
|
over 4 years ago
|
| Allows subnamespace in `for in` |
|
More...
|
over 4 years ago
|
| Merge branch 'fix-check-ce-bench' into 'master' |
|
More...
|
over 4 years ago
|
| Expose type Counterexample.ce_summary |
|
More...
|
over 4 years ago
|
| Check for oracle file using `-e` |
|
More...
|
over 4 years ago
|
| Merge branch '521-allow-user-to-customize-drivers' into 'master' |
|
More...
|
over 4 years ago
|
| fix other calls to Whyconf.load_driver |
|
More...
|
over 4 years ago
|
| better API |
|
More...
|
over 4 years ago
|
| Add an option to dispatch negated goals in RAC |
|
More...
|
over 4 years ago
|
| Choose representation of arrays as terms by environment variable |
|
More...
|
over 4 years ago
|
| Separate logical and program function Array.make |
|
More...
|
over 4 years ago
|
| Stricter SMT model parsing |
|
More...
|
over 4 years ago
|
| Clean CE before handling contradictory VCs, make value cleaning customizable |
|
More...
|
over 4 years ago
|
| Retain CE definitions without element as unparsed |
|
More...
|
over 4 years ago
|
| coincidence_count example: added a bag version |
|
More...
|
almost 5 years ago
|
| stdlib: added bag intersection |
|
More...
|
almost 5 years ago
|
| coincidence_count example: make it nicer using auto deref |
|
More...
|
almost 5 years ago
|
| binary_search: make it nicer with auto deref |
|
More...
|
almost 5 years ago
|
| Coq: added a WhyType instance for type set.Fset.fset |
|
More...
|
almost 5 years ago
|
| Merge branch '517-remove-axioms-in-int-minmax-only-for-z3' into 'master' |
|
More...
|
almost 5 years ago
|
