MARCHE Claude f21055da62 Merge branch 'ease-bitvec-arithmetic' into 'master' ...

Fcilitate proof of arithmetic on bitvectors by Alt-Ergo

See merge request why3/why3!1016

2024-02-20 11:10:11 +01:00

..

alt_ergo_smt

support for Alt-Ergo with Dolmen front-end and SMT syntax

2023-11-16 19:34:49 +00:00

check-ce

Merge branch 'ease-bitvec-arithmetic' into 'master'

2024-02-20 11:10:11 +01:00

encoding

Discriminate algebraic types.

2023-01-31 01:46:10 +01:00

extraction

Resolve "Simplification of record types with only one field"

2023-11-23 14:13:37 +00:00

ide

ide-bench: update cursor position in bench

2019-10-01 14:59:29 +02:00

infer

improved efficiency of BDD-infer

2023-04-28 09:58:02 +02:00

interp

attempt to fix MPFR error in execution tests on reals

2022-04-20 08:57:59 +02:00

invalid

Parser: emit a warning on redundant "import"

2018-06-15 17:08:09 +02:00

memlimit

Delete unused test file for memlimit

2022-05-23 10:51:59 +02:00

parsing/bad

Cause parsing-bench to properly error out and add missing oracles.

2021-02-02 14:22:34 +01:00

plugins

Add regression test

2023-04-25 11:57:38 +02:00

programs

Forbid using different names for constructors, fields, and (co)inductive cases

2023-01-26 14:20:10 +01:00

replay

add a meta to mark a symbol as never removed by remove_unused*

2023-06-15 15:18:48 +00:00

steplimit

Fix regexps for detection of step limit reached

2021-04-19 09:46:34 +00:00

typing

Forbid using different names for constructors, fields, and (co)inductive cases

2023-01-26 14:20:10 +01:00

valid

Resolve "Add injectivity for type invariant"

2024-01-31 13:02:13 +00:00

z3_nombqi

Session create: don't do split_vc by default

2023-10-09 11:25:16 +00:00

bddinfer-bench

move oracles in a separate subdir

2022-07-19 16:41:36 +02:00

bench

split_string: extraction to OCaml

2024-01-24 19:52:46 +01:00

ce-stats.py

fix python script for statistics on CE bench

2024-02-12 13:31:06 +01:00

check_realizations.sh

Use a single Isabelle driver for realizations.

2021-06-29 07:27:35 +02:00

check-ce-bench

Do not silently fail on parse error during CE parsing

2024-01-23 12:41:45 +00:00

copy_oracles.sh

Only one script for CE bench

2022-10-20 16:48:13 +02:00

ide-bench

Use the dispatch executable for testing.

2020-10-21 16:04:06 +02:00

infer-bench

move oracles in a separate subdir

2022-07-19 16:41:36 +02:00

parsing-bench

Cause parsing-bench to properly error out and add missing oracles.

2021-02-02 14:22:34 +01:00

test_mlw_printer

Remove the warning for not modified variables used under old with an attribute

2022-02-17 16:44:02 +01:00

true_goal.why

encoding_decorate : ajout de goal, mono, inst mais assert false sur eux

2010-06-15 16:34:44 +00:00