Matteo Manighetti 445595866e Merge remote-tracking branch 'why3-inria/move_concrete_terms_out_of_parser' into why3-devel

2025-03-25 17:48:51 +01:00

..

bitvec

update sessions

2024-11-03 11:48:13 +01:00

bv

update sessions

2024-11-03 11:48:13 +01:00

ceil

Resolve "Remove axioms in Z3 and CVC4 drivers"

2023-09-01 15:47:33 +00:00

colibri2

Support for colibri2

2024-05-28 11:15:53 +02:00

coq

Support for Coq 8.19.2

2024-10-03 11:19:54 +02:00

coq-interval

Support for Coq 8.19.2

2024-10-03 11:19:54 +02:00

cvc3

Fix session timings on moloch

2023-10-23 09:18:45 +02:00

div

Upgrade sessions to use Alt-Ergo 2.6.0

2025-01-14 19:48:35 +01:00

div_real

disabled Alt-Ergo FPA for versions < 2.5.4 (bug known)

2024-05-23 11:17:31 +02:00

dreal

fix sessions and CE oracles

2024-11-14 14:48:30 +01:00

gappa

Fix session timings on moloch

2023-10-23 09:18:45 +02:00

ieee_float

Upgrade sessions to use Alt-Ergo 2.6.0

2025-01-14 19:48:35 +01:00

metitarski

Fix sessions

2024-04-25 13:10:12 +02:00

polypaver

Fix sessions

2024-04-25 13:10:12 +02:00

real_from_int

fix session having extra edited files

2024-09-18 15:42:05 +02:00

signed_bv

Merge remote-tracking branch 'why3-inria/master' into why3-devel

2024-12-13 17:34:11 +01:00

strings

Upgrade sessions to use Alt-Ergo 2.6.0

2025-01-14 19:48:35 +01:00

zeros

fix obsolete sessions

2024-10-27 17:46:42 +01:00

bitvec.mlw

Add functions sdiv and srem in bitvector theories.

2021-02-06 12:44:27 +01:00

bv.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

ceil.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

colibri2.mlw

Support for colibri2

2024-05-28 11:15:53 +02:00

coq-interval.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

coq.why

…

cvc3.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

div_real.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

div.why

Merge remote-tracking branch 'origin/master' into computer_division_for_master

2018-06-21 23:01:11 +02:00

dreal.mlw

max_int and max_real values not defined as an axiom

2023-04-04 13:00:22 +00:00

gappa.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

ieee_float.mlw

Remove some trailing spaces.

2024-12-07 09:01:55 +01:00

metitarski.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

polypaver.why

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

real_from_int.mlw

check that real.FromInt.from_int is correctly sent to Alt-Ergo

2024-09-17 10:44:53 +02:00

signed_bv.mlw

Several renamings and fix a few pre and post-conditions

2021-09-29 08:57:02 +02:00

strings.mlw

String theory: change [] to s_at (at is a why3 reserved keyword)

2020-01-24 15:43:50 +01:00

zeros.mlw

Support for CVC5

2022-06-03 16:30:54 +00:00