fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
authorFrançois Bobot <francois@bobot.eu>
Fri, 30 Nov 2012 11:35:02 +0000 (11:35 +0000)
committerFrançois Bobot <francois@bobot.eu>
Fri, 30 Nov 2012 11:35:02 +0000 (11:35 +0000)
commit4643949ff4f1586935dfc2607931f26604422b50
tree26c983d56bea5b5112d70ef60766ff4ca99c71f0
parentc157f7e381d4fa2a713796b42a10562112952904
fix the syntax of assert-rewrite/-propagation/-reduction by putting the pattern first
just after the bindings

 Do it before the release in order to not break user files later
19 files changed:
src/parser/smt2/Smt2.g
test/regress/regress0/rewriterules/datatypes2.smt2
test/regress/regress0/rewriterules/datatypes3.smt2
test/regress/regress0/rewriterules/datatypes_clark.smt2
test/regress/regress0/rewriterules/length_gen_010.smt2
test/regress/regress0/rewriterules/native_arrays.smt2
test/regress/regress0/rewriterules/reachability_back_to_the_future.smt2
test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2
test/regress/regress0/rewriterules/relation.smt2
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt [deleted file]
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2 [new file with mode: 0644]
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt [deleted file]
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2 [new file with mode: 0644]
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt [deleted file]
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2 [new file with mode: 0644]
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt [deleted file]
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2 [new file with mode: 0644]