seq « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	intseq.smt2	825	log plain
-rw-r--r--	intseq_dt.smt2	2023	log plain
-rw-r--r--	issue4370-bool-terms.smt2	813	log plain
-rw-r--r--	issue5543-unit-cmv.smt2	357	log plain
-rw-r--r--	issue5547-seq-len-unit.smt2	269	log plain
-rw-r--r--	issue5547-small-seq-len-unit.smt2	207	log plain
-rw-r--r--	issue5665-invalid-model.smt2	329	log plain
-rw-r--r--	issue6337-seq.smt2	325	log plain
-rw-r--r--	len_simplify.smt2	140	log plain
-rw-r--r--	quant_len_trigger.smt2	483	log plain
-rw-r--r--	seq-2var.smt2	138	log plain
-rw-r--r--	seq-ex1.smt2	210	log plain
-rw-r--r--	seq-ex2.smt2	254	log plain
-rw-r--r--	seq-ex3.smt2	562	log plain
-rw-r--r--	seq-ex4.smt2	235	log plain
-rw-r--r--	seq-ex5-dd.smt2	225	log plain
-rw-r--r--	seq-ex5.smt2	238	log plain
-rw-r--r--	seq-expand-defs.smt2	370	log plain
-rw-r--r--	seq-nemp.smt2	158	log plain
-rw-r--r--	seq-nth-uf-z.smt2	324	log plain
-rw-r--r--	seq-nth-uf.smt2	346	log plain
-rw-r--r--	seq-nth-undef-unsat.smt2	521	log plain
-rw-r--r--	seq-nth.smt2	174	log plain
-rw-r--r--	seq-rewrites.smt2	677	log plain
-rw-r--r--	seq-types.smt2	238	log plain