/test/regress/regress0/
../
arith
arr1.smt2
arr1.smtv1.smt2
arr2.smtv1.smt2
array-const-real-parse.smt2
arrayinuf_declare.smt2
arrays
aufbv
auflia
bool
boolean-prec.cvc.smt2
boolean-terms-bug-array.smt2
boolean-terms-kernel1.smt2
boolean-terms.cvc.smt2
bt-test-00.smt2
bt-test-01.smt2
bug1247.smt2
bug161.smtv1.smt2
bug164.smtv1.smt2
bug167.smtv1.smt2
bug168.smtv1.smt2
bug187.smt2
bug217.smt2
bug220.smt2
bug239.smtv1.smt2
bug274.cvc.smt2
bug288.smtv1.smt2
bug288b.smtv1.smt2
bug288c.smtv1.smt2
bug303.smt2
bug310.cvc.smt2
bug32.cvc.smt2
bug322.cvc.smt2
bug322b.cvc.smt2
bug339.smt2
bug365.smt2
bug382.smt2
bug383.smt2
bug398.smt2
bug421.smt2
bug421b.smt2
bug480.smt2
bug484.smt2
bug486.cvc.smt2
bug49.smtv1.smt2
bug512.minimized.smt2
bug521.minimized.smt2
bug522.smt2
bug528a.smt2
bug541.smt2
bug544.smt2
bug548a.smt2
bug576.smt2
bug576a.smt2
bug578.smt2
bug586.cvc.smt2
bug595.cvc.smt2
bug596.cvc.smt2
bug596b.cvc.smt2
bug605.cvc.smt2
bug639.smt2
buggy-ite.smt2
bv
chained-equality.smt2
constant-rewrite.smtv1.smt2
cores
cvc-rerror-print.cvc.smt2
cvc3-bug15.cvc.smt2
cvc3.userdoc.01.cvc.smt2
cvc3.userdoc.02.cvc.smt2
cvc3.userdoc.03.cvc.smt2
cvc3.userdoc.04.cvc.smt2
cvc3.userdoc.05.cvc.smt2
cvc3.userdoc.06.cvc.smt2
datatypes
decision
declare-fun-is-match.smt2
declare-funs.smt2
define-fun-model.smt2
distinct.smtv1.smt2
dump-unsat-core-full.smt2
echo.smt2
eqrange0.smt2
eqrange1.smt2
eqrange2.smt2
eqrange3.smt2
expect
flet.smtv1.smt2
flet2.smtv1.smt2
fmf
fp
fuzz_1.smtv1.smt2
fuzz_3.smtv1.smt2
get-value-incremental.smt2
get-value-ints.smt2
get-value-reals-ints.smt2
get-value-reals.smt2
ho
hung10_itesdk_output1.smt2
hung13sdk_output1.smt2
incorrect1.smtv1.smt2
ineq_basic.smtv1.smt2
ineq_slack.smtv1.smt2
int-to-bv
issue1063-overloading-dt-cons.smt2
issue1063-overloading-dt-fun.smt2
issue1063-overloading-dt-sel.smt2
issue2832-qualId.smt2
issue4010-sort-inf-var.smt2
issue4469-unc-no-reuse-var.smt2
issue4707-bv-to-bool-small.smt2
issue5099-model-1.smt2
issue5099-model-2.smt2
issue5144-resetAssertions.smt2
issue5187-div-justification.smt2
issue5370.smt2
issue5462.smt2
issue5473.smt2
issue5540-2-dump-model.smt2
issue5540-model-decls.smt2
issue5550-num-children.smt2
issue5736.smt2
issue5743.smt2
issue5947.smt2
issue6605-2-abd-triv.smt2
issue6738.smt2
issue6741.smt2
ite.cvc.smt2
ite.smt2
ite2.smt2
ite3.smt2
ite4.smt2
ite_arith.smt2
ite_real_int_type.smtv1.smt2
ite_real_valid.smtv1.smt2
lang_opts_2_6_1.smt2
lemmas
let.cvc.smt2
let.smtv1.smt2
let2.smtv1.smt2
logops.01.cvc.smt2
logops.02.cvc.smt2
logops.03.cvc.smt2
logops.04.cvc.smt2
logops.05.cvc.smt2
model-core.smt2
models-print-1.smt2
models-print-2.smt2
named-expr-use.smt2
nl
opt-abd-no-use.smt2
options
parallel-let.smt2
parser
precedence
preprocess
print_define_fun_internal.smt2
print_lambda.cvc.smt2
print_model.cvc.smt2
printer
proofs
push-pop
quantifiers
rec-fun-const-parse-bug.smt2
rels
sep
seq
sets
simple-dump-model.smt2
simple-lra.smt2
simple-lra.smtv1.smt2
simple-rdl.smt2
simple-rdl.smtv1.smt2
simple-uf.smt2
simple-uf.smtv1.smt2
simple.cvc.smt2
simple.smtv1.smt2
simple2.smtv1.smt2
simplification_bug.smtv1.smt2
simplification_bug2.smtv1.smt2
smallcnf.cvc.smt2
smt2output.smt2
smtlib
strings
sygus
symmetric.smtv1.smt2
test11.cvc.smt2
test9.cvc.smt2
tptp
uf
uf20-03.cvc.smt2
uflia
uflra
unconstrained
use_approx
wiki.01.cvc.smt2
wiki.02.cvc.smt2
wiki.03.cvc.smt2
wiki.04.cvc.smt2
wiki.05.cvc.smt2
wiki.06.cvc.smt2
wiki.07.cvc.smt2
wiki.08.cvc.smt2
wiki.09.cvc.smt2
wiki.10.cvc.smt2
wiki.11.cvc.smt2
wiki.12.cvc.smt2
wiki.13.cvc.smt2
wiki.14.cvc.smt2
wiki.15.cvc.smt2
wiki.16.cvc.smt2
wiki.17.cvc.smt2
wiki.18.cvc.smt2
wiki.19.cvc.smt2
wiki.20.cvc.smt2
wiki.21.cvc.smt2