Amelioration in sequence theory (!67) · Merge requests · pub / colibrics · GitLab

François Bobot requested to merge hra/nseq_theory_for_merge into master Jul 16, 2024

and other related stuff:

avoid slow convergence
fix completeness-bug in pivot with constant
Simplify \forall x. A \implies \forall y. B into \forall x y. A \implies B

Regression:

QF_LRA/spider_benchmarks/op_seen_more1.induction.smt2
QF_UFIDL/pete2/c6nidw_s.smt2
unsat/union/union-Union-leqtqtvc_13.psmt2
unsat/union/union-Union-leqtqtvc_16.psmt2
union/union-Union-ltqtqtvc_13.psmt2
unsat/union/union-Union-ltqtqtvc_16.psmt2