Commit Graph

Select branches

Hide Pull Requests

17

18-sustained

18.0

18.1

18.2

19-sustained

19.0

19.1

19.2

20-sustained

20.0

20.1

20.2

21-sustained

21.0

21.1

21.2

22-sustained

22.0

22.1

22.2

23-sustained

23.0

23.1

23.2

24-sustained

24.0

24.1

24.2

25-sustained

25.0

25.1

25.2

26.0

26.1

26.2

a2c2-2020

fsf

fsf-11.2

fsf-12

fsf-13

fsf-14

fsf-15

gpl-2013

gpl-2014

gpl-2015

gpl-2016

gpl-2017

gpl-2018

lri-colibri

lri-float_test

lri-itp

lri-master

lri-spark-float-smtlib

lts-18

lts-19

lts-20

lts-21

master

newsystem

oxford_cde

spark-14.0

spark-15.0

spark-16.0

why3_polymorphism_smt

#3

fsf-15.1.0

Mono Color

• 774aa26ca1 Merge branch 'topic/no-issue-clochard-cleanup-warning' into 'master' Martin Clochard 2025-04-07 09:35:57 +00:00
• 3fcfd2ed47 Add ada_parsers.conflicts to .gitignore Martin Clochard 2025-04-07 11:31:54 +02:00
• d29be55424 Clean up compiler warnings Martin Clochard 2025-04-07 11:25:36 +02:00
• 48ea53ad63 Merge branch 'topic/kanig-677-cesteps' into 'master' Johannes Kanig 2025-04-07 08:33:38 +00:00
• 5e2f9b047d Merge branch 'vampire-detect' into 'master' Guillaume Melquiond 2025-04-02 12:44:56 +02:00
• ef4680ca53 Change detection order to favor recent versions of Vampire. Guillaume Melquiond 2025-04-02 10:57:01 +02:00
• 4c16f2c8a9 Pass limit pased on CE prover to RAC Johannes Kanig 2025-04-02 17:41:43 +09:00
• 6a1bfa4125 Merge branch 'topic/kanig-890-coq' into 'master' Johannes Kanig 2025-03-31 07:36:10 +00:00
• 7fc06eaa52 Revert "get rid of deprecated module Arith.Div2" Johannes Kanig 2025-03-31 09:35:26 +09:00
• bccba6e9cb Merge branch 'improvements-to-rac' into 'master' Matteo Manighetti 2025-03-28 14:03:34 +01:00
• ff0fbb7dfe Merge branch 'why3-devel' into 'master' Matteo Manighetti 2025-03-27 09:55:57 +00:00
• 2e931cf017 Update oracles Matteo Manighetti 2025-03-26 23:10:05 +01:00
• beb0f3e826 Use computed attributes and kinds in concrete element Matteo Manighetti 2025-03-25 18:11:50 +01:00
• b5b6a8b904 Fail more gently if term arg can't be interpreted Matteo Manighetti 2025-03-26 17:55:05 +01:00
• 52cc1f8f72 Merge branch 'rac-failure-log-environment' into 'master' MARCHE Claude 2025-03-27 08:36:53 +01:00
• 7d669f1054 fix bench rac oracle Claude Marche 2025-03-26 19:31:07 +01:00
• 2946be39dc Compute the kind of reconstructed model elements Matteo Manighetti 2025-03-26 18:28:58 +01:00
• 82a377837f Fail more gently if term arg can't be interpreted Matteo Manighetti 2025-03-26 17:55:05 +01:00
• 2742dd04ec Merge branch 'set_iterators' into 'master' MARCHE Claude 2025-03-26 17:20:01 +01:00
• 997bdc53c1 add simple examples of iterators on sets with extraction to OCaml MARCHE Claude 2025-03-26 17:20:01 +01:00
• 222b2e0fcd fix printing of execution logs Claude Marche 2025-03-26 17:12:15 +01:00
• 2c82a040a2 Merge branch 'fix_bddinfer_warnings' into 'master' MARCHE Claude 2025-03-26 15:50:13 +01:00
• 534bd32d04 Do not introduce program variables for zero and one in int.Int module Claude Marche 2025-03-26 14:13:47 +01:00
• 6af6614833 minor: suppress warnings due to labeled argument Claude Marche 2025-03-26 13:56:45 +01:00
• 5761aaee73 Use computed attributes in concrete element Matteo Manighetti 2025-03-25 18:11:50 +01:00
• 68e7bfe1a3 Get concrete terms when RAC not executed Matteo Manighetti 2025-03-24 16:19:42 +01:00
• 1dede98289 Disable warning on concrete terms Matteo Manighetti 2025-03-12 11:05:46 +01:00
• 32bda2a925 Emit warning when concrete term conversion fails Matteo Manighetti 2025-03-12 11:05:28 +01:00
• ddc59fa212 RAC: build concrete floats; improve global env Matteo Manighetti 2025-03-10 14:36:28 +01:00
• 8fdfd8feea RAC: Log all variables at failure Matteo Manighetti 2025-03-06 14:03:06 +01:00
• 9d2cf502df Merge remote-tracking branch 'why3-inria/master' into why3-devel Matteo Manighetti 2025-03-03 15:44:38 +01:00
• 399658bd65 Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel Matteo Manighetti 2025-03-03 11:02:40 +01:00
• fb74e3e332 Interpreter: create values for real logic constants Matteo Manighetti 2025-02-19 14:16:39 +01:00
• a4c510a653 Adapt to new check_ce interface Matteo Manighetti 2025-02-17 16:51:17 +01:00
• 445595866e Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel Matteo Manighetti 2025-02-17 16:32:17 +01:00
• 0590797db8 Merge branch 'master' into why3-devel Matteo Manighetti 2024-12-20 17:58:03 +01:00
• f39e24ed74 Merge branch 'master' into why3-devel Matteo Manighetti 2024-12-20 17:58:03 +01:00
• 16cb82ac56 Merge branch 'topic/kanig-866-altergosmt' into 'master' Johannes Kanig 2025-03-24 10:21:10 +00:00
• 389fdf8840 Merge branch 'example-alpha-beta' into 'master' Jean-Christophe Filliâtre 2025-03-21 11:57:51 +01:00
• ce8aab11f2 Merge branch 'example-union-find' into 'master' Jean-Christophe Filliâtre 2025-03-21 11:24:02 +01:00
• 8037b67cec new example: alpha-beta Jean-Christophe Filliatre 2025-03-21 10:08:09 +01:00
• 1d36796166 new example: union-find Jean-Christophe Filliatre 2025-03-21 10:05:02 +01:00
• 9c6f54fbba Merge branch 'improve_log_sum_exp' into 'master' MARCHE Claude 2025-03-14 16:58:28 +01:00
• 816b76b5fe Cleaning the proof and the doc comments for publications on the gallery Claude Marche 2025-03-12 13:56:35 +01:00
• 57742895f4 New driver for Alt-ergo SMT, gnatprove style Johannes Kanig 2025-03-10 17:52:18 +09:00
• 1710e595fd Merge branch 'fix-clone-injectivity' into 'master' François Bobot 2025-03-13 17:32:37 +01:00
• 1809f7f99a Fix clone injectivity Benjamin Jorge 2025-03-13 15:54:10 +01:00
• 763b4f7f75 Expose bug Benjamin Jorge 2025-03-13 15:53:52 +01:00
• 77b54e3a00 Cleanup Matteo Manighetti 2025-03-13 11:23:11 +01:00
• 1d974677c5 Emit warning when concrete term conversion fails Matteo Manighetti 2025-03-12 11:05:28 +01:00
• b8a4cfb714 Update oracles Matteo Manighetti 2025-03-07 11:19:56 +01:00
• 34d839f1a3 RAC: Log all variables at failure Matteo Manighetti 2025-03-06 14:03:06 +01:00
• b16e1bc131 Merge branch 'improve-rac-on-floats' into 'master' MARCHE Claude 2025-03-10 19:29:37 +01:00
• 47d9343a9f Merge branch 'log-sum-exp' into 'master' MARCHE Claude 2025-03-10 18:11:32 +01:00
• e1d543c06f SLSE full proof Claude Marche 2025-02-18 17:57:54 +01:00
• 88cd302542 RAC: build concrete floats; improve global env Matteo Manighetti 2025-03-10 14:36:28 +01:00
• 4a84d8bf3d Merge branch 'counterexamples_parse_poly' into 'master' MARCHE Claude 2025-03-07 11:28:43 +01:00
• 5cec133cd5 Improve counterexample parsing: reconstruct polymorphic instances Matteo Manighetti 2025-03-07 11:28:42 +01:00
• ca98a663c3 Merge branch '896-misleading-error-message' into 'master' MARCHE Claude 2025-03-05 18:38:35 +01:00
• 4dbd7a6cf6 Merge branch 'file-not-found-exception' into 'master' Guillaume Melquiond 2025-03-05 18:10:26 +01:00
• fdc3d390f1 do not say "syntax error" since it is a typing error Claude Marche 2025-03-05 15:57:49 +01:00
• 43c3e236d0 do not say "syntax error" since it is a typing error Claude Marche 2025-03-05 15:57:49 +01:00
• 3a057a137c Merge branch 'move_concrete_terms_out_of_parser' into 'master' MARCHE Claude 2025-03-03 15:25:34 +01:00
• 82ec599640 restored API example for counterexamples Claude Marche 2025-03-03 13:06:24 +01:00
• e4671018c3 Check_ce: only use known map for concrete term conversion Matteo Manighetti 2025-03-03 11:32:37 +01:00
• 3ded61b16b fix remaining warnings and CE oracles for UNDEFINED value Claude Marche 2025-03-03 11:26:10 +01:00
• a912f9d0f7 fix conversion of term to concrete terms for records Claude Marche 2025-02-28 11:49:39 +01:00
• 9cfa339ada Adapt counterexample example to check_ce API Matteo Manighetti 2025-02-28 10:44:12 +01:00
• 15f05dabe0 Check_ce: build concrete terms from prover model Matteo Manighetti 2025-02-27 17:49:56 +01:00
• b6e18e5bc7 fix printing of concrete terms Claude Marche 2025-02-27 15:39:26 +01:00
• 5ca58690f9 more strict translation of term to record concrete term term Claude Marche 2025-02-27 15:24:19 +01:00
• 9c053cea1f fix CE oracle Claude Marche 2025-02-27 13:31:06 +01:00
• cbc6d1272d Merge branch 'topic/448-dross-program_exit' into 'master' Claire Dross 2025-02-27 10:09:33 +00:00
• 18d0a65d51 fix oracle for rgf/Z3 Claude Marche 2025-02-27 10:42:58 +01:00
• ed463237d9 Update oracles with concrete_terms from check_ce Matteo Manighetti 2025-02-24 17:38:49 +01:00
• 4c8545b762 Don't create concrete_terms in smtv2_model_parser Matteo Manighetti 2025-02-24 17:38:32 +01:00
• 935fb739ea Interpreter: create values for real logic constants Matteo Manighetti 2025-02-19 14:16:39 +01:00
• 8e3522958a do not extra check on type of fields Claude Marche 2025-02-14 17:18:13 +01:00
• 7e28f7d616 More careful dummy model element Matteo Manighetti 2025-02-14 16:50:37 +01:00
• 66f231086f get record fields from the theory instead of the module Claude Marche 2025-02-14 16:46:46 +01:00
• 4e56c0000f fix detction of records: must have exactly one constructor Claude Marche 2025-02-14 16:21:19 +01:00
• 03b7f41e91 More careful check of record type Matteo Manighetti 2025-02-14 16:13:09 +01:00
• fbd4ff90c0 Fix floats in check_ce Matteo Manighetti 2025-02-14 15:55:20 +01:00
• 99af329aa4 Fix bv_length in concrete floats Matteo Manighetti 2025-02-14 15:04:55 +01:00
• f0ae859329 Some work on floats Matteo Manighetti 2025-02-14 14:46:34 +01:00
• 736b6f0179 Update oracles Matteo Manighetti 2025-02-14 08:53:42 +01:00
• bb458db0b6 Convert concrete epsilon terms in check_ce and not in model_parser Matteo Manighetti 2025-02-14 08:53:14 +01:00
• a97a3b2168 Add new VC_Kinds in gnat_expl.ml Claire Dross 2025-01-17 13:24:18 +01:00
• 6694da2ad8 fix wrong addition to mli Claude Marche 2025-02-23 14:55:54 +01:00
• 814b18fcc0 allow again the support of BDD-infer Claude Marche 2025-02-09 20:56:27 +01:00
• 669c7d84b4 Merge branch '900-reactivate-bdd-infer' into 'master' MARCHE Claude 2025-02-21 18:47:00 +01:00
• 93ef37caa1 allow again the support of BDD-infer Claude Marche 2025-02-09 20:56:27 +01:00
• 7357576150 Merge branch 'space-leak' into 'master' Guillaume Melquiond 2025-02-21 11:08:33 +01:00
• 852a021041 Improve compatibility with C23 (fix #901). Guillaume Melquiond 2025-02-20 17:35:20 +01:00
• 2c88539bc9 Merge branch 'topic/kanig-856-inline' into 'master' Johannes Kanig 2025-02-20 09:17:48 +00:00
• b6058c6cf0 Robustify code that saves inlining context Johannes Kanig 2025-02-19 19:33:20 +09:00
• 091926fcfa do not extra check on type of fields Claude Marche 2025-02-14 17:18:13 +01:00
• 9a68b27bcd More careful dummy model element Matteo Manighetti 2025-02-14 16:50:37 +01:00
• ad5b51eca8 get record fields from the theory instead of the module Claude Marche 2025-02-14 16:46:46 +01:00
• f820613b6c fix detction of records: must have exactly one constructor Claude Marche 2025-02-14 16:21:19 +01:00