[Quantifier] Fix useless application criteria
The consequence was missing congruence closure
Showing
- src_colibri2/core/egraph.ml 2 additions, 2 deletionssrc_colibri2/core/egraph.ml
- src_colibri2/core/ground.ml 7 additions, 3 deletionssrc_colibri2/core/ground.ml
- src_colibri2/tests/solve/all/unsat/dune.inc 3 additions, 0 deletionssrc_colibri2/tests/solve/all/unsat/dune.inc
- src_colibri2/tests/solve/all/unsat/lost_in_search_union.psmt2 1 addition, 1 deletion...colibri2/tests/solve/all/unsat/lost_in_search_union.psmt2
- src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2 1 addition, 1 deletionsrc_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
- src_colibri2/tests/solve/all/unsat/union-Union-interqtvc_5.psmt2 740 additions, 0 deletions...ibri2/tests/solve/all/unsat/union-Union-interqtvc_5.psmt2
- src_colibri2/theories/quantifier/info.ml 0 additions, 2 deletionssrc_colibri2/theories/quantifier/info.ml
- src_colibri2/theories/quantifier/quantifier.ml 14 additions, 18 deletionssrc_colibri2/theories/quantifier/quantifier.ml
- src_common/union.mlw 4 additions, 4 deletionssrc_common/union.mlw
- src_common/union/why3session.xml 89 additions, 172 deletionssrc_common/union/why3session.xml
Loading
Please register or sign in to comment