Matteo Manighetti eddcb30d72 Update Alt-Ergo 2.3.x proofs

2023-08-28 14:17:52 +02:00

..

alt-ergo-models

Initial bulk upgrade of z3

2023-04-13 09:43:18 +00:00

bv-smtlib-realization

fix sessions

2021-06-25 10:26:57 +02:00

func_literals

Update Alt-Ergo 2.3.x proofs

2023-08-28 14:17:52 +02:00

ignore

upgrade bench scripts with CVC5 from 1.0.0 to 1.0.5, upgrade sessions

2023-07-11 15:13:50 +02:00

lemma_functions

Initial bulk upgrade of z3

2023-04-13 09:43:18 +00:00

replay

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

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

test_elim

Initial bulk upgrade of z3

2023-04-13 09:43:18 +00:00

test_projections

Initial bulk upgrade of z3

2023-04-13 09:43:18 +00:00

times2float

Update Alt-Ergo 2.3.x proofs

2023-08-28 14:17:52 +02:00

alt-ergo-models.mlw

stdlib, examples: remove redundant "import"

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

alt-ergo-models.why

stdlib, examples: remove redundant "import"

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

array-test.mlw

stdlib, examples: remove redundant "import"

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

bitvector-test.why

stdlib, examples: remove redundant "import"

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

bv-smtlib-realization.why

stdlib, examples: remove redundant "import"

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

execute-tests.mlw

fix pinterp output and update benchs

2020-06-25 09:27:21 +02:00

func_literals.mlw

function literals examples

2020-11-13 10:04:04 +01:00

hashtbl-test.mlw

stdlib, examples: remove redundant "import"

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

ignore.mlw

support for SMTLIB's minimize command

2023-07-03 16:19:46 +00:00

int32-test.mlw

stdlib, examples: remove redundant "import"

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

lemma_functions.mlw

stdlib, examples: remove redundant "import"

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

matrix-test.mlw

stdlib, examples: remove redundant "import"

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

pqueue-test.mlw

library: several changes in pqueue

2019-07-02 17:07:21 +02:00

queue-test.mlw

updated proof sessions

2019-06-05 17:55:47 +02:00

rac.mlw

Add meta compute_max_steps in rac.mlw to avoid

2022-11-08 15:05:09 +01:00

rac.oracle

do not call git in bench script, use another file for RAC oracle

2023-04-12 13:36:59 +02:00

random-test.mlw

stdlib, examples: remove redundant "import"

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

regexp-test.why

stdlib, examples: remove redundant "import"

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

replay.mlw

avoid warning "axiom does not contains abstract local symbols"

2020-08-26 10:33:54 +02:00

stack-test.mlw

stdlib, examples: remove redundant "import"

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

test_elim.mlw

more dependency metas

2022-06-02 09:44:06 +02:00

test_projections.mlw

Add test.

2023-01-09 09:18:55 +01:00

times2float.mlw

move basic example into tests directory

2020-08-25 13:34:56 +02:00