| Add oracle for real_values test |
|
More...
|
over 2 years ago
|
| Handle epsilon terms for projections |
|
More...
|
over 2 years ago
|
| Update oracles, CE was false before |
|
More...
|
over 2 years ago
|
| Handle Vterm (Tconst) in big_int_of_value |
|
More...
|
over 2 years ago
|
| List of fields for constructor may be empty |
|
More...
|
over 2 years ago
|
| Update some oracles after checking the diffs |
|
More...
|
over 2 years ago
|
| Merge branch 'merge_bdd_infer_again' into 'master' |
|
More...
|
over 2 years ago
|
| BDD-infer: add a drop statement to drop proxy vars as early as possible |
|
More...
|
over 2 years ago
|
| Merge branch 'merge_bdd_infer' into 'master' |
|
More...
|
over 2 years ago
|
| Support for the match construct in smtv2 printer. |
|
More...
|
over 2 years ago
|
| New version of BDD infer: |
|
More...
|
over 2 years ago
|
| Update oracles for which the diff is ok |
|
More...
|
over 2 years ago
|
| Check sort when parsing array value |
|
More...
|
over 2 years ago
|
| Cleanup |
|
More...
|
over 2 years ago
|
| Fix some compilation warnings |
|
More...
|
over 2 years ago
|
| Cleanup |
|
More...
|
over 2 years ago
|
| Update printer to handle Ttrue/Tfalse with type ty_bool coming from CE values |
|
More...
|
over 2 years ago
|
| Prover variables may have the same name if the sort is different |
|
More...
|
over 2 years ago
|
| Cache evaluated values for variables / Clean remaining prover variables |
|
More...
|
over 2 years ago
|
| Merge branch 'bddinfer_support_for_break' into 'master' |
|
More...
|
over 2 years ago
|
| Merge branch 'unused-unused' into 'master' |
|
More...
|
over 2 years ago
|
| Support for `break` in BDDinfer |
|
More...
|
over 2 years ago
|
| More informative error messages |
|
More...
|
over 2 years ago
|
| Merge branch 'dreal' into 'master' |
|
More...
|
over 2 years ago
|
| Specific treatment for builtin lsymbols |
|
More...
|
over 2 years ago
|
| Disable test "maps_mono". |
|
More...
|
over 2 years ago
|
| Add default value for reals in RAC |
|
More...
|
over 2 years ago
|
| Elements of fractions in SMT models can be integer or real values |
|
More...
|
over 2 years ago
|
| Avoid declaring as unused variables that are already unused. |
|
More...
|
over 2 years ago
|
| Remove dependency on Alt-Ergo 2.3.3 (fix #618). |
|
More...
|
over 2 years ago
|
