[Quant] Fix forall in forall
Remains a todo with type substitution
Showing
- src_colibri2/tests/solve/smt_quant/unsat/dune.inc 2 additions, 0 deletionssrc_colibri2/tests/solve/smt_quant/unsat/dune.inc
- src_colibri2/tests/solve/smt_quant/unsat/forall8.smt2 12 additions, 0 deletionssrc_colibri2/tests/solve/smt_quant/unsat/forall8.smt2
- src_colibri2/theories/LRA/delta.ml 2 additions, 0 deletionssrc_colibri2/theories/LRA/delta.ml
- src_colibri2/theories/quantifier/InvertedPath.ml 9 additions, 1 deletionsrc_colibri2/theories/quantifier/InvertedPath.ml
- src_colibri2/theories/quantifier/InvertedPath.mli 5 additions, 0 deletionssrc_colibri2/theories/quantifier/InvertedPath.mli
- src_colibri2/theories/quantifier/PN.ml 10 additions, 0 deletionssrc_colibri2/theories/quantifier/PN.ml
- src_colibri2/theories/quantifier/PN.mli 3 additions, 0 deletionssrc_colibri2/theories/quantifier/PN.mli
- src_colibri2/theories/quantifier/pattern.ml 20 additions, 6 deletionssrc_colibri2/theories/quantifier/pattern.ml
- src_colibri2/theories/quantifier/pattern.mli 5 additions, 2 deletionssrc_colibri2/theories/quantifier/pattern.mli
- src_colibri2/theories/quantifier/quantifier.ml 49 additions, 24 deletionssrc_colibri2/theories/quantifier/quantifier.ml
- src_colibri2/theories/quantifier/trigger.ml 21 additions, 4 deletionssrc_colibri2/theories/quantifier/trigger.ml
Loading
Please register or sign in to comment