| Clean some warning messages. |
|
More...
|
almost 3 years ago
|
| Merge branch 'fix-702' into 'master' |
|
More...
|
almost 3 years ago
|
| keep_only_arithmetic transform : Implication instanciation ok |
|
More...
|
almost 3 years ago
|
| Raise LibraryNotFound whenever possible (fix #702). |
|
More...
|
almost 3 years ago
|
| Merge branch '695_remove_unused' into 'master' |
|
More...
|
almost 3 years ago
|
| Improve "remove_unused" transformation |
|
More...
|
almost 3 years ago
|
| Started to add support for the instanciation of implication |
|
More...
|
almost 3 years ago
|
| Merge branch '699-bad-lexing-for-separation-of-commands' into 'master' |
|
More...
|
almost 3 years ago
|
| Empty bound variables when interpreting a new function |
|
More...
|
almost 3 years ago
|
| Update oracles |
|
More...
|
almost 3 years ago
|
| Move remaining files in bench/ce to bench/check-ce or bench/check-ce-xfail |
|
More...
|
almost 3 years ago
|
| fixed command-line lexing |
|
More...
|
almost 3 years ago
|
| Less declarations thrown away in keep_only_arithmetic transformation |
|
More...
|
almost 3 years ago
|
| Reverted experimental change |
|
More...
|
almost 3 years ago
|
| Deleted printer dreal, we use the smtv2 printer instead |
|
More...
|
almost 3 years ago
|
| Added some tests for dreal |
|
More...
|
almost 3 years ago
|
| Add type_fields in printing_info to reconstruct records from CE models |
|
More...
|
almost 3 years ago
|
| Experimental support for keep_only_arithmetic tactic |
|
More...
|
almost 3 years ago
|
| Allow quantified assertions in keep_only_arithmetic |
|
More...
|
almost 3 years ago
|
| When importing a model value of the form Tapp (ls,args) check if ls is a constructor |
|
More...
|
almost 3 years ago
|
| Create Qannotident (i.e. with sort) for prover variables |
|
More...
|
almost 3 years ago
|
| Transformation keep_only_arithmetic corrected |
|
More...
|
almost 3 years ago
|
| Store records and bound vars in maps |
|
More...
|
almost 3 years ago
|
| Improved keep_only_arithmetic transformation |
|
More...
|
almost 3 years ago
|
| disable use of -p for profiling with OCaml >= 4.09 |
|
More...
|
almost 3 years ago
|
| (WIP) Handling of prover variables |
|
More...
|
almost 3 years ago
|
| update sessions |
|
More...
|
almost 3 years ago
|
| Merge branch 'fixed_introduce_premises' into 'master' |
|
More...
|
almost 3 years ago
|
| Introduction: treat the introduced axioms in the same way as Skolem constants |
|
More...
|
almost 3 years ago
|
| gallery: improved list reversal |
|
More...
|
almost 3 years ago
|
