| fixed introduce_premises |
|
More...
|
almost 3 years ago
|
| Add WIP comments for dealing with types inside variable names |
|
More...
|
almost 3 years ago
|
| Add new transformation keep_only_arithmetic |
|
More...
|
almost 3 years ago
|
| Use pinfo.constructors when parsing SMT models for variables and applications |
|
More...
|
almost 3 years ago
|
| When importing a model value, handle references for which expected type and actual type of term do not match |
|
More...
|
almost 3 years ago
|
| Remove simplify_trivial_quantification from colibri drivers |
|
More...
|
almost 3 years ago
|
| Merge branch '252-check-counterexamples-benchmark' into 'master' |
|
More...
|
almost 3 years ago
|
| Suppress useless transformations |
|
More...
|
almost 3 years ago
|
| More debug messages for smtv2_parser |
|
More...
|
almost 3 years ago
|
| More complete parsing of datatype_decl in SMT models, to be used for records |
|
More...
|
almost 3 years ago
|
| dReal driver : Corrected some bugs |
|
More...
|
almost 3 years ago
|
| Replace name by model_trace attribute before creating model_element |
|
More...
|
almost 3 years ago
|
| dreal printer : only handle equality for ints and reals |
|
More...
|
almost 3 years ago
|
| Improvements of dreal printer |
|
More...
|
almost 3 years ago
|
| Print type and value for CE models / Cleanup |
|
More...
|
almost 3 years ago
|
| Handle cases where the condition of an if expression is not reduced to true / false |
|
More...
|
almost 3 years ago
|
| Move algebraic_types_mono, recursive_model and simple_array from ce to check-ce bench |
|
More...
|
almost 3 years ago
|
| Merge branch '640-model-term-without-location-leads-to-a-failure-of-the-rac-prover' into 'master' |
|
More...
|
almost 3 years ago
|
| update check-ce oracles (6 new confirmed CE) |
|
More...
|
almost 3 years ago
|
| Merge branch 'master' into 640-model-term-without-location-leads-to-a-failure-of-the-rac-prover |
|
More...
|
almost 3 years ago
|
| Merged origin branch |
|
More...
|
almost 3 years ago
|
| Merge branch '691-reduce-the-size-of-check-ce-oracles' into 'master' |
|
More...
|
almost 3 years ago
|
| Rename --verbosity option into --ce-log-verbosity |
|
More...
|
almost 3 years ago
|
| generated function for a goal is a let with a unit body |
|
More...
|
almost 3 years ago
|
| Use loc when creating fresh rs for goals |
|
More...
|
almost 3 years ago
|
| get location also when there is no model_vc_post attribute |
|
More...
|
almost 3 years ago
|
| (Check_ce] RAC should also execute goals |
|
More...
|
almost 3 years ago
|
| Reduce size of oracles in check-ce bench |
|
More...
|
almost 3 years ago
|
| Merge branch '682-broken-ide-support-for-python-files' into 'master' |
|
More...
|
almost 3 years ago
|
| Merge branch 'remove_unused_pow2' into 'master' |
|
More...
|
almost 3 years ago
|
