Fix various regression tests (#1657)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 21 Mar 2018 16:41:50 +0000 (09:41 -0700)
committerGitHub <noreply@github.com>
Wed, 21 Mar 2018 16:41:50 +0000 (09:41 -0700)
commitbe2702490d684c100ba6abe76ee156078a9aa621
tree8b22bc7e38aad39da092b409dded4d2ce84b4047
parent8f0aae827e16f4dfcebb8dad2cc528649d40b16a
Fix various regression tests (#1657)

While reorganizing the regression tests, I found three tests with a
wrong status, one that CVC4 reported unknown for and some regression
tests that had command line options set in the Makefile.am instead of
the tests themselves. This commit fixes the status of the three
regression tests (verified the status with Z3), adds command line
options to make the previously "unknown" test work, and moves the
command line options from the Makefile.am into the individual regression
tests. The latter also required some minor changes to the regression
script because it would not try to determine the expected output from
the (set-info :status ...) command if there was one directive (such as
EXPECT/COMMAND-LINE/etc.).  This was an issue with the tests that now
have a COMMAND-LINE directive.
94 files changed:
test/regress/regress0/rewriterules/Makefile.am
test/regress/regress0/rewriterules/datatypes.smt2
test/regress/regress0/rewriterules/datatypes_clark.smt2
test/regress/regress0/rewriterules/length.smt2
test/regress/regress0/rewriterules/length_gen_n.smt2
test/regress/regress0/rewriterules/length_gen_n_lemma.smt2
test/regress/regress0/rewriterules/length_trick.smt2
test/regress/regress0/rewriterules/length_trick2.smt2
test/regress/regress0/rewriterules/native_arrays.smt2
test/regress/regress0/rewriterules/native_datatypes.smt2
test/regress/regress0/rewriterules/relation.smt2
test/regress/regress0/rewriterules/simulate_rewriting.smt2
test/regress/regress0/uf/Makefile.am
test/regress/regress0/uf/pred.smt
test/regress/regress0/unconstrained/Makefile.am
test/regress/regress0/unconstrained/arith.smt2
test/regress/regress0/unconstrained/arith2.smt2
test/regress/regress0/unconstrained/arith3.smt2
test/regress/regress0/unconstrained/arith4.smt2
test/regress/regress0/unconstrained/arith5.smt2
test/regress/regress0/unconstrained/arith6.smt2
test/regress/regress0/unconstrained/arith7.smt2
test/regress/regress0/unconstrained/array1.smt2
test/regress/regress0/unconstrained/bvbool.smt2
test/regress/regress0/unconstrained/bvbool2.smt2
test/regress/regress0/unconstrained/bvbool3.smt2
test/regress/regress0/unconstrained/bvcmp.smt2
test/regress/regress0/unconstrained/bvconcat.smt2
test/regress/regress0/unconstrained/bvconcat2.smt2
test/regress/regress0/unconstrained/bvdiv.smt2
test/regress/regress0/unconstrained/bvext.smt2
test/regress/regress0/unconstrained/bvite.smt2
test/regress/regress0/unconstrained/bvmul.smt2
test/regress/regress0/unconstrained/bvmul2.smt2
test/regress/regress0/unconstrained/bvmul3.smt2
test/regress/regress0/unconstrained/bvnot.smt2
test/regress/regress0/unconstrained/bvsle.smt2
test/regress/regress0/unconstrained/bvsle2.smt2
test/regress/regress0/unconstrained/bvsle3.smt2
test/regress/regress0/unconstrained/bvsle4.smt2
test/regress/regress0/unconstrained/bvsle5.smt2
test/regress/regress0/unconstrained/bvslt.smt2
test/regress/regress0/unconstrained/bvslt2.smt2
test/regress/regress0/unconstrained/bvslt3.smt2
test/regress/regress0/unconstrained/bvslt4.smt2
test/regress/regress0/unconstrained/bvslt5.smt2
test/regress/regress0/unconstrained/bvule.smt2
test/regress/regress0/unconstrained/bvule2.smt2
test/regress/regress0/unconstrained/bvule3.smt2
test/regress/regress0/unconstrained/bvule4.smt2
test/regress/regress0/unconstrained/bvule5.smt2
test/regress/regress0/unconstrained/bvult.smt2
test/regress/regress0/unconstrained/bvult2.smt2
test/regress/regress0/unconstrained/bvult3.smt2
test/regress/regress0/unconstrained/bvult4.smt2
test/regress/regress0/unconstrained/bvult5.smt2
test/regress/regress0/unconstrained/geq.smt2
test/regress/regress0/unconstrained/gt.smt2
test/regress/regress0/unconstrained/ite.smt2
test/regress/regress0/unconstrained/leq.smt2
test/regress/regress0/unconstrained/lt.smt2
test/regress/regress0/unconstrained/mult1.smt2
test/regress/regress0/unconstrained/uf1.smt2
test/regress/regress0/unconstrained/xor.smt2
test/regress/regress1/quantifiers/Makefile.am
test/regress/regress1/quantifiers/set3.smt2
test/regress/regress1/rewriterules/Makefile.am
test/regress/regress1/rewriterules/datatypes2.smt2
test/regress/regress1/rewriterules/datatypes3.smt2
test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2
test/regress/regress1/rewriterules/datatypes_sat.smt2
test/regress/regress1/rewriterules/length_gen.smt2
test/regress/regress1/rewriterules/length_gen_010.smt2
test/regress/regress1/rewriterules/length_gen_010_lemma.smt2
test/regress/regress1/rewriterules/length_gen_020.smt2
test/regress/regress1/rewriterules/length_gen_020_sat.smt2
test/regress/regress1/rewriterules/length_gen_040.smt2
test/regress/regress1/rewriterules/length_gen_040_lemma.smt2
test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2
test/regress/regress1/rewriterules/length_gen_080.smt2
test/regress/regress1/rewriterules/length_gen_160_lemma.smt2
test/regress/regress1/rewriterules/length_gen_inv_160.smt2
test/regress/regress1/rewriterules/length_trick3.smt2
test/regress/regress1/rewriterules/length_trick3_int.smt2
test/regress/regress1/rewriterules/reachability_back_to_the_future.smt2
test/regress/regress1/rewriterules/read5.smt2
test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2
test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2
test/regress/regress1/rewriterules/test_guards.smt2
test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2
test/regress/regress2/Makefile.am
test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2
test/regress/run_regression