ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
23.2
why3/drivers
History
Solène Moreau 3eec8efaef (V610-014) Disable simplify_trivial_quantification in colibri driver 
Disabling this transformation significantly speeds up the runtime of
the testsuite with only minor proof regressions.

Change-Id: I85d2694654378e25535d70dd7673eb39493e2185
Depends-On: I5972b19c9e392f1480f18143d30db00e87942b5a
2022-08-09 09:00:46 +02:00
..
alt_ergo_2_2_0.drv
Resolve "Add support for Alt-Ergo 2.4.0"
2021-02-05 14:46:11 +01:00
alt_ergo_2_3.drv
Resolve "Add support for Alt-Ergo 2.4.0"
2021-02-05 14:46:11 +01:00
alt_ergo_common.drv
(V719-014) Merging Inria/master into SPARK/master
2022-07-19 14:57:03 +02:00
alt_ergo_fp.drv
U622-016 Update Alt-Ergo driver
2021-12-15 08:23:13 +09:00
alt_ergo_model.drv
…
alt_ergo_smt2.drv
…
alt_ergo.drv
(V721-016) Reactivate remove_unused_keep_constants in drivers
2022-07-28 15:27:03 +02:00
alt-ergo_gnatprove.drv
(V721-016) Enable remove_unused_keep_constants in gnatprove drivers.
2022-07-29 09:50:32 +02:00
beagle.drv
…
colibri2.drv
[Colibri2] add sqrt
2022-03-17 14:03:07 +01:00
colibri.drv
(V610-014) Disable simplify_trivial_quantification in colibri driver
2022-08-09 09:00:46 +02:00
coq_gnatprove.drv
…
coq-common.gen
…
coq-realize.drv
…
coq-ssreflect.drv
Support for multi-line strings. Drivers updated accordingly.
2019-10-21 14:13:59 +02:00
coq.drv
…
cvc3.drv
…
cvc4_14.drv
V516-003 Merging Inria master into SPARK master
2022-06-15 14:15:27 +02:00
cvc4_15_counterexample.drv
…
cvc4_15.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
cvc4_16_counterexample.drv
…
cvc4_16.drv
Drivers updated - string theory is not mapped to CVC4 1.6
2019-11-06 13:55:34 +01:00
cvc4_16.gen
(V721-016) Reactivate remove_unused_keep_constants in drivers
2022-07-28 15:27:03 +02:00
cvc4_17_counterexample.drv
CVC4 strings-counterexample prover
2020-04-01 17:09:06 +01:00
cvc4_17.drv
For CVC4 1.7 do not use --string-exp flag by default
2020-03-26 15:42:33 +01:00
cvc4_18_strings_counterexample.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
cvc4_18_strings.drv
Resolve "Fix drivers for SMT-LIB strings"
2022-04-06 14:29:41 +00:00
cvc4_bv.gen
T127-015 Merge with upstream Why3
2021-09-07 13:50:44 +02:00
cvc4_gnatprove_ce.drv
…
cvc4_gnatprove_extra_axioms.drv
…
cvc4_gnatprove_oldfloat.drv
…
cvc4_gnatprove_qf.drv
T127-015 fix drivers after merge
2021-02-19 17:38:21 +09:00
cvc4_gnatprove.drv
…
cvc4-realize.drv
V516-003 Merging Inria master into SPARK master
2022-06-15 14:15:27 +02:00
cvc4.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
cvc5_counterexample.drv
Support for CVC5
2022-06-03 16:30:54 +00:00
cvc5_gnatprove_ce.drv
V516-003 Add cvc5 driver for CE
2022-06-21 12:10:39 +02:00
cvc5_gnatprove.drv
V204-033 add driver and steps config for cvc5g
2022-02-11 17:32:53 +00:00
cvc5.drv
Add outofmemory pattern for CVC5
2022-06-07 09:36:41 +02:00
discrimination.gen
Repair discriminate2
2021-04-08 12:26:07 +00:00
eprover.drv
…
gappa.drv
UC02-020 remove part of gappa driver
2021-12-16 19:02:49 +09:00
iprover.drv
…
isabelle-common.gen
Adapted to Isabelle2019
2020-03-03 09:58:48 +01:00
isabelle-realize.drv
Use a single Isabelle driver for realizations.
2021-06-29 07:27:35 +02:00
isabelle.drv
Use a single Isabelle driver for realizations.
2021-06-29 07:27:35 +02:00
mathematica.drv
…
mathsat.drv
…
metis.drv
…
metitarski.drv
…
no-bv.gen
…
polypaver.drv
…
princess.drv
…
psyche.drv
…
pvs-common.gen
…
pvs-realize.drv
…
pvs.drv
…
safeprover.drv
…
simplify.drv
…
smt-libv2-bv-realization.gen
Add new drivers for z3 and cvc4 to support bitvectors of size 128 and 256
2021-07-12 13:08:49 +02:00
smt-libv2-bv.gen
V325-031 Merge with upstream Why3
2022-03-29 10:47:33 +02:00
smt-libv2-floats-gnatprove.gen
…
smt-libv2-floats-int_via_bv.gen
…
smt-libv2-floats-int_via_real.gen
…
smt-libv2-floats.gen
UB05-006 Add theories and drivers for extended floats
2021-11-08 15:28:43 +01:00
smt-libv2-gnatprove.gen
…
smt-libv2.gen
SA24-015 Remove properties in int.MinMax only for Z3
2020-12-18 09:14:48 +01:00
smtlib-strings.gen
Resolve "Fix drivers for SMT-LIB strings"
2022-04-06 14:29:41 +00:00
spass_types.drv
…
spass.drv
…
tptp-tff0.drv
…
tptp-tff1.drv
…
tptp.gen
…
vampire-smt.drv
make transf eliminate_definition aware of the meta for CE tracing
2021-07-15 11:18:57 +02:00
vampire.drv
…
verit.drv
…
why3_smt.drv
make transf eliminate_definition aware of the meta for CE tracing
2021-07-15 11:18:57 +02:00
why3_tptp.drv
…
why3.drv
…
yices-smt2.drv
…
yices.drv
…
z3_432.drv
Add memlimit section in the bench
2022-05-19 16:13:12 +02:00
z3_440_counterexample.drv
…
z3_440.drv
(V721-016) Reactivate remove_unused_keep_constants in drivers
2022-07-28 15:27:03 +02:00
z3_471_counterexample.drv
Drivers updated so strings are only used with solvers that support them
2019-11-05 16:19:09 +01:00
z3_471_nobv.drv
Drivers updated so strings are only used with solvers that support them
2019-11-05 16:19:09 +01:00
z3_471.drv
Drivers updated so strings are only used with solvers that support them
2019-11-05 16:19:09 +01:00
z3_bv.gen
T824-034 U721-028 Complete CVC4 and Z3 drivers for 256bits
2021-07-22 11:31:22 +02:00
z3_gnatprove_ce.drv
(V721-016) Enable remove_unused_keep_constants in gnatprove drivers.
2022-07-29 09:50:32 +02:00
z3_gnatprove.drv
(V721-016) Enable remove_unused_keep_constants in gnatprove drivers.
2022-07-29 09:50:32 +02:00
z3_no_quant.drv
T127-015 fix drivers after merge
2021-02-19 17:38:21 +09:00
z3_smtv1.drv
…
z3.drv
…
zenon_modulo.drv
…
zenon.drv
…