MARCHE Claude 715fa89d16 separate transformations for intros, dequant, and remove_unused ...

remove unused before reflection transformation

avoid subst to a unused symbol

2023-04-25 12:20:08 +00: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

Initial bulk upgrade of z3

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

lemma_functions

Initial bulk upgrade of z3

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

replay

separate transformations for intros, dequant, and remove_unused

2023-04-25 12:20:08 +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

Initial bulk upgrade of z3

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

alt-ergo-models.mlw

…

alt-ergo-models.why

…

array-test.mlw

…

bitvector-test.why

…

bv-smtlib-realization.why

…

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

…

int32-test.mlw

…

lemma_functions.mlw

…

matrix-test.mlw

…

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

…

regexp-test.why

…

replay.mlw

avoid warning "axiom does not contains abstract local symbols"

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

stack-test.mlw

…

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