Johannes Kanig 62a9f30bd5 VB10-088 include power axioms ...

The axioms and lemmas in the BVAda module (mostly related to power)
were systematically suppressed. We now add them back. They are
removed automatically if the goal doesn't contain the relevant
symbols (such as power).

Change-Id: I4d2c4e1e622fdf7d2d156a9060de55dfb0e8926d

2022-11-14 17:33:32 +09:00

..

alt_ergo_2_2_0.drv

…

alt_ergo_2_3.drv

…

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

…

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

…

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_17.drv

…

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

…

cvc4_gnatprove_ce.drv

…

cvc4_gnatprove_extra_axioms.drv

…

cvc4_gnatprove_oldfloat.drv

…

cvc4_gnatprove_qf.drv

…

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

…

eprover.drv

…

gappa.drv

UC02-020 remove part of gappa driver

2021-12-16 19:02:49 +09:00

iprover.drv

…

isabelle-common.gen

…

isabelle-realize.drv

…

isabelle.drv

…

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

…

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

VB10-088 include power axioms

2022-11-14 17:33:32 +09:00

smt-libv2.gen

…

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

…

vampire.drv

…

verit.drv

…

why3_smt.drv

…

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

…

z3_471_nobv.drv

…

z3_471.drv

…

z3_bv.gen

…

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

…

z3_smtv1.drv

…

z3.drv

…

zenon_modulo.drv

…

zenon.drv

…