Rewrite gentest and merge models and dolmen into default tag

Halbaroth · Oct 8, 2024 · 6405283 · 6405283
1 parent 967ac13
commit 6405283
Show file tree

Hide file tree

Showing 231 changed files with 4 additions and 434 deletions.
diff --git a/tests/bitv/testfile-array-cs.dolmen.smt2 b/tests/bitv/testfile-array-cs.dolmen.smt2
diff --git a/tests/bitv/testfile-bv2nat-delayed.dolmen.smt2 b/tests/bitv/testfile-bv2nat-delayed.dolmen.smt2
diff --git a/tests/bitv/testfile-bv2nat-immediate.dolmen.expected b/tests/bitv/testfile-bv2nat-immediate.dolmen.expected
diff --git a/tests/bitv/testfile-bv2nat-immediate.dolmen.smt2 b/tests/bitv/testfile-bv2nat-immediate.dolmen.smt2
diff --git a/tests/bitv/testfile-bv2nat-models.dolmen.expected b/tests/bitv/testfile-bv2nat-models.dolmen.expected
diff --git a/tests/bitv/testfile-bv2nat-models.dolmen.smt2 b/tests/bitv/testfile-bv2nat-models.dolmen.smt2
diff --git a/tests/bitv/testfile-bvadd-001.dolmen.expected b/tests/bitv/testfile-bvadd-001.dolmen.expected
diff --git a/tests/bitv/testfile-bvadd-001.dolmen.smt2 b/tests/bitv/testfile-bvadd-001.dolmen.smt2
diff --git a/tests/bitv/testfile-bvadd-002.dolmen.expected b/tests/bitv/testfile-bvadd-002.dolmen.expected
diff --git a/tests/bitv/testfile-bvadd-002.dolmen.smt2 b/tests/bitv/testfile-bvadd-002.dolmen.smt2
diff --git a/tests/bitv/testfile-bvand-001.dolmen.expected b/tests/bitv/testfile-bvand-001.dolmen.expected
diff --git a/tests/bitv/testfile-bvand-001.dolmen.smt2 b/tests/bitv/testfile-bvand-001.dolmen.smt2
diff --git a/tests/bitv/testfile-bvnot-term.dolmen.smt2 b/tests/bitv/testfile-bvnot-term.dolmen.smt2
diff --git a/tests/bitv/testfile-bvnot.dolmen.expected → tests/bitv/testfile-bvnot.default.expected b/tests/bitv/testfile-bvnot.dolmen.expected → tests/bitv/testfile-bvnot.default.expected
diff --git a/tests/bitv/testfile-bvnot.dolmen.smt2 → tests/bitv/testfile-bvnot.default.smt2 b/tests/bitv/testfile-bvnot.dolmen.smt2 → tests/bitv/testfile-bvnot.default.smt2
diff --git a/tests/bitv/testfile-bvor-001.dolmen.expected b/tests/bitv/testfile-bvor-001.dolmen.expected
diff --git a/tests/bitv/testfile-bvor-001.dolmen.smt2 b/tests/bitv/testfile-bvor-001.dolmen.smt2
diff --git a/tests/bitv/testfile-bvsub-001.dolmen.expected b/tests/bitv/testfile-bvsub-001.dolmen.expected
diff --git a/tests/bitv/testfile-bvsub-001.dolmen.smt2 b/tests/bitv/testfile-bvsub-001.dolmen.smt2
diff --git a/tests/bitv/testfile-bvsub-002.dolmen.expected b/tests/bitv/testfile-bvsub-002.dolmen.expected
diff --git a/tests/bitv/testfile-bvsub-002.dolmen.smt2 b/tests/bitv/testfile-bvsub-002.dolmen.smt2
diff --git a/tests/bitv/testfile-bvxor-001.dolmen.expected b/tests/bitv/testfile-bvxor-001.dolmen.expected
diff --git a/tests/bitv/testfile-bvxor-001.dolmen.smt2 b/tests/bitv/testfile-bvxor-001.dolmen.smt2
diff --git a/tests/bitv/testfile-int2bv-delayed.dolmen.expected b/tests/bitv/testfile-int2bv-delayed.dolmen.expected
diff --git a/tests/bitv/testfile-int2bv-delayed.dolmen.smt2 b/tests/bitv/testfile-int2bv-delayed.dolmen.smt2
diff --git a/tests/bitv/testfile-int2bv-immediate.dolmen.expected b/tests/bitv/testfile-int2bv-immediate.dolmen.expected
diff --git a/tests/bitv/testfile-int2bv-immediate.dolmen.smt2 b/tests/bitv/testfile-int2bv-immediate.dolmen.smt2
diff --git a/tests/bitv/testfile-qfbv-timeout.unix.dolmen.expected b/tests/bitv/testfile-qfbv-timeout.unix.dolmen.expected
diff --git a/tests/bitv/testfile-qfbv-timeout.unix.dolmen.smt2 b/tests/bitv/testfile-qfbv-timeout.unix.dolmen.smt2
diff --git a/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 b/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2
diff --git a/tests/dolmen/bitv/bv2nat_bvnot.dolmen.expected b/tests/dolmen/bitv/bv2nat_bvnot.dolmen.expected
diff --git a/tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2 b/tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2
diff --git a/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.expected b/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.expected
diff --git a/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.smt2 b/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.smt2
diff --git a/tests/dolmen/bitv/coherence.dolmen.expected b/tests/dolmen/bitv/coherence.dolmen.expected
diff --git a/tests/dolmen/bitv/coherence.dolmen.smt2 b/tests/dolmen/bitv/coherence.dolmen.smt2
diff --git a/tests/dolmen/bitv/cyclic.dolmen.expected b/tests/dolmen/bitv/cyclic.dolmen.expected
diff --git a/tests/dolmen/bitv/cyclic.dolmen.smt2 b/tests/dolmen/bitv/cyclic.dolmen.smt2
diff --git a/tests/dolmen/bitv/not-contra.dolmen.expected b/tests/dolmen/bitv/not-contra.dolmen.expected
diff --git a/tests/dolmen/bitv/not-contra.dolmen.smt2 b/tests/dolmen/bitv/not-contra.dolmen.smt2
diff --git a/tests/dolmen/bitv/notextract.dolmen.expected b/tests/dolmen/bitv/notextract.dolmen.expected
diff --git a/tests/dolmen/bitv/notextract.dolmen.smt2 b/tests/dolmen/bitv/notextract.dolmen.smt2
diff --git a/tests/dolmen/bitv/notnotx.dolmen.expected b/tests/dolmen/bitv/notnotx.dolmen.expected
diff --git a/tests/dolmen/bitv/notnotx.dolmen.smt2 b/tests/dolmen/bitv/notnotx.dolmen.smt2
diff --git a/tests/dolmen/bitv/notx.dolmen.expected b/tests/dolmen/bitv/notx.dolmen.expected
diff --git a/tests/dolmen/bitv/notx.dolmen.smt2 b/tests/dolmen/bitv/notx.dolmen.smt2
diff --git a/tests/float/test_float1.dolmen.expected b/tests/float/test_float1.dolmen.expected
diff --git a/tests/float/test_float1.dolmen.smt2 b/tests/float/test_float1.dolmen.smt2
diff --git a/tests/float/test_float2.models.expected → tests/float/test_float2.default.expected b/tests/float/test_float2.models.expected → tests/float/test_float2.default.expected
diff --git a/tests/float/test_float2.models.smt2 → tests/float/test_float2.default.smt2 b/tests/float/test_float2.models.smt2 → tests/float/test_float2.default.smt2
diff --git a/tests/issues/issue1024.err.dolmen.expected → tests/issues/1024.err.default.expected b/tests/issues/issue1024.err.dolmen.expected → tests/issues/1024.err.default.expected
diff --git a/tests/issues/issue1024.err.dolmen.smt2 → tests/issues/1024.err.default.smt2 b/tests/issues/issue1024.err.dolmen.smt2 → tests/issues/1024.err.default.smt2
diff --git a/tests/issues/1163.models.expected → tests/issues/1163.default.expected b/tests/issues/1163.models.expected → tests/issues/1163.default.expected
diff --git a/tests/issues/1163.models.smt2 → tests/issues/1163.default.smt2 b/tests/issues/1163.models.smt2 → tests/issues/1163.default.smt2
diff --git a/tests/issues/555.models.expected → tests/issues/555.default.expected b/tests/issues/555.models.expected → tests/issues/555.default.expected
diff --git a/tests/issues/555.models.smt2 → tests/issues/555.default.smt2 b/tests/issues/555.models.smt2 → tests/issues/555.default.smt2
diff --git a/tests/issues/649/649.dolmen.smt2 b/tests/issues/649/649.dolmen.smt2
diff --git a/tests/issues/664/664.dolmen.smt2 b/tests/issues/664/664.dolmen.smt2
diff --git a/tests/issues/777.models.expected → tests/issues/777.default.expected b/tests/issues/777.models.expected → tests/issues/777.default.expected
diff --git a/tests/issues/777.models.smt2 → tests/issues/777.default.smt2 b/tests/issues/777.models.smt2 → tests/issues/777.default.smt2
diff --git a/tests/issues/854/function.models.expected → tests/issues/854/function.default.expected b/tests/issues/854/function.models.expected → tests/issues/854/function.default.expected
diff --git a/tests/issues/854/function.models.smt2 → tests/issues/854/function.default.smt2 b/tests/issues/854/function.models.smt2 → tests/issues/854/function.default.smt2
diff --git a/tests/issues/854/original.models.expected → tests/issues/854/original.default.expected b/tests/issues/854/original.models.expected → tests/issues/854/original.default.expected
diff --git a/tests/issues/854/original.models.smt2 → tests/issues/854/original.default.smt2 b/tests/issues/854/original.models.smt2 → tests/issues/854/original.default.smt2
diff --git a/tests/issues/854/twice_eq.models.expected → tests/issues/854/twice_eq.default.expected b/tests/issues/854/twice_eq.models.expected → tests/issues/854/twice_eq.default.expected
diff --git a/tests/issues/854/twice_eq.models.smt2 → tests/issues/854/twice_eq.default.smt2 b/tests/issues/854/twice_eq.models.smt2 → tests/issues/854/twice_eq.default.smt2
diff --git a/tests/issues/883.dolmen.expected b/tests/issues/883.dolmen.expected
diff --git a/tests/issues/883.dolmen.smt2 b/tests/issues/883.dolmen.smt2
diff --git a/tests/issues/926.models.expected → tests/issues/926.default.expected b/tests/issues/926.models.expected → tests/issues/926.default.expected
diff --git a/tests/issues/926.models.smt2 → tests/issues/926.default.smt2 b/tests/issues/926.models.smt2 → tests/issues/926.default.smt2
diff --git a/tests/models/adt/arith.models.expected → tests/models/adt/arith.default.expected b/tests/models/adt/arith.models.expected → tests/models/adt/arith.default.expected
diff --git a/tests/models/adt/arith.models.smt2 → tests/models/adt/arith.default.smt2 b/tests/models/adt/arith.models.smt2 → tests/models/adt/arith.default.smt2
diff --git a/tests/models/adt/list.models.expected → tests/models/adt/list.default.expected b/tests/models/adt/list.models.expected → tests/models/adt/list.default.expected
diff --git a/tests/models/adt/list.models.smt2 → tests/models/adt/list.default.smt2 b/tests/models/adt/list.models.smt2 → tests/models/adt/list.default.smt2
diff --git a/tests/models/adt/rec.models.expected → tests/models/adt/rec.default.expected b/tests/models/adt/rec.models.expected → tests/models/adt/rec.default.expected
diff --git a/tests/models/adt/rec.models.smt2 → tests/models/adt/rec.default.smt2 b/tests/models/adt/rec.models.smt2 → tests/models/adt/rec.default.smt2
diff --git a/tests/models/adt/rec2.models.expected → tests/models/adt/rec2.default.expected b/tests/models/adt/rec2.models.expected → tests/models/adt/rec2.default.expected
diff --git a/tests/models/adt/rec2.models.smt2 → tests/models/adt/rec2.default.smt2 b/tests/models/adt/rec2.models.smt2 → tests/models/adt/rec2.default.smt2
diff --git a/tests/models/adt/rec3.models.expected → tests/models/adt/rec3.default.expected b/tests/models/adt/rec3.models.expected → tests/models/adt/rec3.default.expected
diff --git a/tests/models/adt/rec3.models.smt2 → tests/models/adt/rec3.default.smt2 b/tests/models/adt/rec3.models.smt2 → tests/models/adt/rec3.default.smt2
diff --git a/tests/models/adt/small.models.expected → tests/models/adt/small.default.expected b/tests/models/adt/small.models.expected → tests/models/adt/small.default.expected
diff --git a/tests/models/adt/small.models.smt2 → tests/models/adt/small.default.smt2 b/tests/models/adt/small.models.smt2 → tests/models/adt/small.default.smt2
diff --git a/tests/models/arith/arith1.expected → tests/models/arith/arith1.default.expected b/tests/models/arith/arith1.expected → tests/models/arith/arith1.default.expected
diff --git a/tests/models/arith/arith1.models.smt2 → tests/models/arith/arith1.default.smt2 b/tests/models/arith/arith1.models.smt2 → tests/models/arith/arith1.default.smt2
diff --git a/tests/models/arith/arith1.models.expected b/tests/models/arith/arith1.models.expected
diff --git a/tests/models/arith/arith1.smt2 b/tests/models/arith/arith1.smt2
diff --git a/tests/models/arith/arith10.dolmen.expected → tests/models/arith/arith10.default.expected b/tests/models/arith/arith10.dolmen.expected → tests/models/arith/arith10.default.expected
diff --git a/tests/models/arith/arith10.dolmen.smt2 → tests/models/arith/arith10.default.smt2 b/tests/models/arith/arith10.dolmen.smt2 → tests/models/arith/arith10.default.smt2
diff --git a/tests/models/arith/arith11.dolmen.expected → tests/models/arith/arith11.default.expected b/tests/models/arith/arith11.dolmen.expected → tests/models/arith/arith11.default.expected
diff --git a/tests/models/arith/arith11.dolmen.smt2 → tests/models/arith/arith11.default.smt2 b/tests/models/arith/arith11.dolmen.smt2 → tests/models/arith/arith11.default.smt2
diff --git a/tests/models/arith/arith12.dolmen.expected → tests/models/arith/arith12.default.expected b/tests/models/arith/arith12.dolmen.expected → tests/models/arith/arith12.default.expected
diff --git a/tests/models/arith/arith12.dolmen.smt2 → tests/models/arith/arith12.default.smt2 b/tests/models/arith/arith12.dolmen.smt2 → tests/models/arith/arith12.default.smt2
diff --git a/tests/models/arith/arith13.models.expected → tests/models/arith/arith13.default.expected b/tests/models/arith/arith13.models.expected → tests/models/arith/arith13.default.expected
diff --git a/tests/models/arith/arith13.models.smt2 → tests/models/arith/arith13.default.smt2 b/tests/models/arith/arith13.models.smt2 → tests/models/arith/arith13.default.smt2
diff --git a/tests/models/arith/arith14.models.expected → tests/models/arith/arith14.default.expected b/tests/models/arith/arith14.models.expected → tests/models/arith/arith14.default.expected
diff --git a/tests/models/arith/arith14.models.smt2 → tests/models/arith/arith14.default.smt2 b/tests/models/arith/arith14.models.smt2 → tests/models/arith/arith14.default.smt2
diff --git a/tests/models/arith/arith15.models.expected → tests/models/arith/arith15.default.expected b/tests/models/arith/arith15.models.expected → tests/models/arith/arith15.default.expected
diff --git a/tests/models/arith/arith15.models.smt2 → tests/models/arith/arith15.default.smt2 b/tests/models/arith/arith15.models.smt2 → tests/models/arith/arith15.default.smt2
diff --git a/tests/models/arith/arith2.expected → tests/models/arith/arith2.default.expected b/tests/models/arith/arith2.expected → tests/models/arith/arith2.default.expected
diff --git a/tests/models/arith/arith2.models.smt2 → tests/models/arith/arith2.default.smt2 b/tests/models/arith/arith2.models.smt2 → tests/models/arith/arith2.default.smt2
diff --git a/tests/models/arith/arith2.models.expected b/tests/models/arith/arith2.models.expected
diff --git a/tests/models/arith/arith2.smt2 b/tests/models/arith/arith2.smt2
diff --git a/tests/models/arith/arith3.dolmen.expected → tests/models/arith/arith3.default.expected b/tests/models/arith/arith3.dolmen.expected → tests/models/arith/arith3.default.expected
diff --git a/tests/models/arith/arith3.dolmen.smt2 → tests/models/arith/arith3.default.smt2 b/tests/models/arith/arith3.dolmen.smt2 → tests/models/arith/arith3.default.smt2
diff --git a/tests/models/arith/arith4.dolmen.expected → tests/models/arith/arith4.default.expected b/tests/models/arith/arith4.dolmen.expected → tests/models/arith/arith4.default.expected
diff --git a/tests/models/arith/arith4.dolmen.smt2 → tests/models/arith/arith4.default.smt2 b/tests/models/arith/arith4.dolmen.smt2 → tests/models/arith/arith4.default.smt2
diff --git a/tests/models/arith/arith5.dolmen.expected → tests/models/arith/arith5.default.expected b/tests/models/arith/arith5.dolmen.expected → tests/models/arith/arith5.default.expected
diff --git a/tests/models/arith/arith5.dolmen.smt2 → tests/models/arith/arith5.default.smt2 b/tests/models/arith/arith5.dolmen.smt2 → tests/models/arith/arith5.default.smt2
diff --git a/tests/models/arith/arith6.dolmen.expected → tests/models/arith/arith6.default.expected b/tests/models/arith/arith6.dolmen.expected → tests/models/arith/arith6.default.expected
diff --git a/tests/models/arith/arith6.dolmen.smt2 → tests/models/arith/arith6.default.smt2 b/tests/models/arith/arith6.dolmen.smt2 → tests/models/arith/arith6.default.smt2
diff --git a/tests/models/arith/arith7.dolmen.expected → tests/models/arith/arith7.default.expected b/tests/models/arith/arith7.dolmen.expected → tests/models/arith/arith7.default.expected
diff --git a/tests/models/arith/arith7.dolmen.smt2 → tests/models/arith/arith7.default.smt2 b/tests/models/arith/arith7.dolmen.smt2 → tests/models/arith/arith7.default.smt2
diff --git a/tests/models/arith/arith8.dolmen.expected → tests/models/arith/arith8.default.expected b/tests/models/arith/arith8.dolmen.expected → tests/models/arith/arith8.default.expected
diff --git a/tests/models/arith/arith8.dolmen.smt2 → tests/models/arith/arith8.default.smt2 b/tests/models/arith/arith8.dolmen.smt2 → tests/models/arith/arith8.default.smt2
diff --git a/tests/models/arith/arith9.dolmen.expected → tests/models/arith/arith9.default.expected b/tests/models/arith/arith9.dolmen.expected → tests/models/arith/arith9.default.expected
diff --git a/tests/models/arith/arith9.dolmen.smt2 → tests/models/arith/arith9.default.smt2 b/tests/models/arith/arith9.dolmen.smt2 → tests/models/arith/arith9.default.smt2
diff --git a/tests/models/array/array1.models.expected → tests/models/array/array1.default.expected b/tests/models/array/array1.models.expected → tests/models/array/array1.default.expected
diff --git a/tests/models/array/array1.models.smt2 → tests/models/array/array1.default.smt2 b/tests/models/array/array1.models.smt2 → tests/models/array/array1.default.smt2
diff --git a/...dels/array/embedded-array.models.expected → ...els/array/embedded-array.default.expected b/...dels/array/embedded-array.models.expected → ...els/array/embedded-array.default.expected
diff --git a/...s/models/array/embedded-array.models.smt2 → .../models/array/embedded-array.default.smt2 b/...s/models/array/embedded-array.models.smt2 → .../models/array/embedded-array.default.smt2
diff --git a/tests/models/bitv/bvand-1.models.expected → tests/models/bitv/bvand-1.default.expected b/tests/models/bitv/bvand-1.models.expected → tests/models/bitv/bvand-1.default.expected
diff --git a/tests/models/bitv/bvand-1.models.smt2 → tests/models/bitv/bvand-1.default.smt2 b/tests/models/bitv/bvand-1.models.smt2 → tests/models/bitv/bvand-1.default.smt2
diff --git a/tests/models/bitv/bvand-2.models.expected → tests/models/bitv/bvand-2.default.expected b/tests/models/bitv/bvand-2.models.expected → tests/models/bitv/bvand-2.default.expected
diff --git a/tests/models/bitv/bvand-2.models.smt2 → tests/models/bitv/bvand-2.default.smt2 b/tests/models/bitv/bvand-2.models.smt2 → tests/models/bitv/bvand-2.default.smt2
diff --git a/tests/models/bitv/bvor-1.models.expected → tests/models/bitv/bvor-1.default.expected b/tests/models/bitv/bvor-1.models.expected → tests/models/bitv/bvor-1.default.expected
diff --git a/tests/models/bitv/bvor-1.models.smt2 → tests/models/bitv/bvor-1.default.smt2 b/tests/models/bitv/bvor-1.models.smt2 → tests/models/bitv/bvor-1.default.smt2
diff --git a/tests/models/bitv/bvor-2.models.expected → tests/models/bitv/bvor-2.default.expected b/tests/models/bitv/bvor-2.models.expected → tests/models/bitv/bvor-2.default.expected
diff --git a/tests/models/bitv/bvor-2.models.smt2 → tests/models/bitv/bvor-2.default.smt2 b/tests/models/bitv/bvor-2.models.smt2 → tests/models/bitv/bvor-2.default.smt2
diff --git a/tests/models/bitv/bvxor-1.models.expected → tests/models/bitv/bvxor-1.default.expected b/tests/models/bitv/bvxor-1.models.expected → tests/models/bitv/bvxor-1.default.expected
diff --git a/tests/models/bitv/bvxor-1.models.smt2 → tests/models/bitv/bvxor-1.default.smt2 b/tests/models/bitv/bvxor-1.models.smt2 → tests/models/bitv/bvxor-1.default.smt2
diff --git a/tests/models/bitv/bvxor-2.models.expected → tests/models/bitv/bvxor-2.default.expected b/tests/models/bitv/bvxor-2.models.expected → tests/models/bitv/bvxor-2.default.expected
diff --git a/tests/models/bitv/bvxor-2.models.smt2 → tests/models/bitv/bvxor-2.default.smt2 b/tests/models/bitv/bvxor-2.models.smt2 → tests/models/bitv/bvxor-2.default.smt2
diff --git a/tests/bitv/testfile-array-cs.dolmen.expected → tests/models/bitv/cardinal.default.expected b/tests/bitv/testfile-array-cs.dolmen.expected → tests/models/bitv/cardinal.default.expected
diff --git a/tests/models/bitv/cardinal.models.smt2 → tests/models/bitv/cardinal.default.smt2 b/tests/models/bitv/cardinal.models.smt2 → tests/models/bitv/cardinal.default.smt2
diff --git a/tests/models/bitv/cardinal.models.expected b/tests/models/bitv/cardinal.models.expected
diff --git a/.../models/bitv/cs-soundness.models.expected → ...models/bitv/cs-soundness.default.expected b/.../models/bitv/cs-soundness.models.expected → ...models/bitv/cs-soundness.default.expected
diff --git a/tests/models/bitv/cs-soundness.models.smt2 → tests/models/bitv/cs-soundness.default.smt2 b/tests/models/bitv/cs-soundness.models.smt2 → tests/models/bitv/cs-soundness.default.smt2
diff --git a/tests/models/bitv/extract.models.expected → tests/models/bitv/extract.default.expected b/tests/models/bitv/extract.models.expected → tests/models/bitv/extract.default.expected
diff --git a/tests/models/bitv/extract.models.smt2 → tests/models/bitv/extract.default.smt2 b/tests/models/bitv/extract.models.smt2 → tests/models/bitv/extract.default.smt2
diff --git a/tests/models/bitv/manyslice.models.expected → tests/models/bitv/manyslice.default.expected b/tests/models/bitv/manyslice.models.expected → tests/models/bitv/manyslice.default.expected
diff --git a/tests/models/bitv/manyslice.models.smt2 → tests/models/bitv/manyslice.default.smt2 b/tests/models/bitv/manyslice.models.smt2 → tests/models/bitv/manyslice.default.smt2
diff --git a/tests/models/bitv/not.models.expected → tests/models/bitv/not.default.expected b/tests/models/bitv/not.models.expected → tests/models/bitv/not.default.expected
diff --git a/tests/models/bitv/not.models.smt2 → tests/models/bitv/not.default.smt2 b/tests/models/bitv/not.models.smt2 → tests/models/bitv/not.default.smt2
diff --git a/tests/models/bitv/optim-1.models.expected → tests/models/bitv/optim-1.default.expected b/tests/models/bitv/optim-1.models.expected → tests/models/bitv/optim-1.default.expected
diff --git a/tests/models/bitv/optim-1.models.smt2 → tests/models/bitv/optim-1.default.smt2 b/tests/models/bitv/optim-1.models.smt2 → tests/models/bitv/optim-1.default.smt2
diff --git a/tests/models/bitv/optim-2.models.expected → tests/models/bitv/optim-2.default.expected b/tests/models/bitv/optim-2.models.expected → tests/models/bitv/optim-2.default.expected
diff --git a/tests/models/bitv/optim-2.models.smt2 → tests/models/bitv/optim-2.default.smt2 b/tests/models/bitv/optim-2.models.smt2 → tests/models/bitv/optim-2.default.smt2
diff --git a/tests/models/bitv/optim-3.models.expected → tests/models/bitv/optim-3.default.expected b/tests/models/bitv/optim-3.models.expected → tests/models/bitv/optim-3.default.expected
diff --git a/tests/models/bitv/optim-3.models.smt2 → tests/models/bitv/optim-3.default.smt2 b/tests/models/bitv/optim-3.models.smt2 → tests/models/bitv/optim-3.default.smt2
diff --git a/tests/models/bitv/optim-4.models.expected → tests/models/bitv/optim-4.default.expected b/tests/models/bitv/optim-4.models.expected → tests/models/bitv/optim-4.default.expected
diff --git a/tests/models/bitv/optim-4.models.smt2 → tests/models/bitv/optim-4.default.smt2 b/tests/models/bitv/optim-4.models.smt2 → tests/models/bitv/optim-4.default.smt2
diff --git a/tests/models/bitv/optim-5.models.expected → tests/models/bitv/optim-5.default.expected b/tests/models/bitv/optim-5.models.expected → tests/models/bitv/optim-5.default.expected
diff --git a/tests/models/bitv/optim-5.models.smt2 → tests/models/bitv/optim-5.default.smt2 b/tests/models/bitv/optim-5.models.smt2 → tests/models/bitv/optim-5.default.smt2
diff --git a/tests/models/bitv/specified.models.expected → tests/models/bitv/specified.default.expected b/tests/models/bitv/specified.models.expected → tests/models/bitv/specified.default.expected
diff --git a/tests/models/bitv/specified.models.smt2 → tests/models/bitv/specified.default.smt2 b/tests/models/bitv/specified.models.smt2 → tests/models/bitv/specified.default.smt2
diff --git a/tests/models/bool/bool1.models.expected → tests/models/bool/bool1.default.expected b/tests/models/bool/bool1.models.expected → tests/models/bool/bool1.default.expected
diff --git a/tests/models/bool/bool1.models.smt2 → tests/models/bool/bool1.default.smt2 b/tests/models/bool/bool1.models.smt2 → tests/models/bool/bool1.default.smt2
diff --git a/tests/models/bool/bool2.models.expected → tests/models/bool/bool2.default.expected b/tests/models/bool/bool2.models.expected → tests/models/bool/bool2.default.expected
diff --git a/tests/models/bool/bool2.models.smt2 → tests/models/bool/bool2.default.smt2 b/tests/models/bool/bool2.models.smt2 → tests/models/bool/bool2.default.smt2
diff --git a/tests/models/bool/bool3.models.expected → tests/models/bool/bool3.default.expected b/tests/models/bool/bool3.models.expected → tests/models/bool/bool3.default.expected
diff --git a/tests/models/bool/bool3.models.smt2 → tests/models/bool/bool3.default.smt2 b/tests/models/bool/bool3.models.smt2 → tests/models/bool/bool3.default.smt2
diff --git a/tests/models/check_sat.models.ae → tests/models/check_sat.default.ae b/tests/models/check_sat.models.ae → tests/models/check_sat.default.ae
diff --git a/tests/models/check_sat.models.expected → tests/models/check_sat.default.expected b/tests/models/check_sat.models.expected → tests/models/check_sat.default.expected
diff --git a/tests/models/complete_1.models.expected → tests/models/complete_1.default.expected b/tests/models/complete_1.models.expected → tests/models/complete_1.default.expected
diff --git a/tests/models/complete_1.models.smt2 → tests/models/complete_1.default.smt2 b/tests/models/complete_1.models.smt2 → tests/models/complete_1.default.smt2
diff --git a/tests/models/complete_2.models.expected → tests/models/complete_2.default.expected b/tests/models/complete_2.models.expected → tests/models/complete_2.default.expected
diff --git a/tests/models/complete_2.models.smt2 → tests/models/complete_2.default.smt2 b/tests/models/complete_2.models.smt2 → tests/models/complete_2.default.smt2
diff --git a/tests/models/complete_3.models.expected → tests/models/complete_3.default.expected b/tests/models/complete_3.models.expected → tests/models/complete_3.default.expected
diff --git a/tests/models/complete_3.models.smt2 → tests/models/complete_3.default.smt2 b/tests/models/complete_3.models.smt2 → tests/models/complete_3.default.smt2
diff --git a/tests/models/issues/715/715_1.models.ae → tests/models/issues/715/715_1.default.ae b/tests/models/issues/715/715_1.models.ae → tests/models/issues/715/715_1.default.ae
diff --git a/.../bitv/testfile-bvnot-term.dolmen.expected → .../models/issues/715/715_1.default.expected b/.../bitv/testfile-bvnot-term.dolmen.expected → .../models/issues/715/715_1.default.expected
diff --git a/tests/models/issues/715/715_1.models.expected b/tests/models/issues/715/715_1.models.expected
diff --git a/...s/models/issues/715/715_2.models.expected → .../models/issues/715/715_2.default.expected b/...s/models/issues/715/715_2.models.expected → .../models/issues/715/715_2.default.expected
diff --git a/tests/models/issues/715/715_2.models.smt2 → tests/models/issues/715/715_2.default.smt2 b/tests/models/issues/715/715_2.models.smt2 → tests/models/issues/715/715_2.default.smt2
diff --git a/tests/models/issues/719.models.err.expected → tests/models/issues/719.default.err.expected b/tests/models/issues/719.models.err.expected → tests/models/issues/719.default.err.expected
diff --git a/tests/models/issues/719.models.err.smt2 → tests/models/issues/719.default.err.smt2 b/tests/models/issues/719.models.err.smt2 → tests/models/issues/719.default.err.smt2
diff --git a/tests/models/records/record1.models.expected → ...s/models/records/record1.default.expected b/tests/models/records/record1.models.expected → ...s/models/records/record1.default.expected
diff --git a/tests/models/records/record1.models.smt2 → tests/models/records/record1.default.smt2 b/tests/models/records/record1.models.smt2 → tests/models/records/record1.default.smt2
diff --git a/tests/models/records/record2.models.expected → ...s/models/records/record2.default.expected b/tests/models/records/record2.models.expected → ...s/models/records/record2.default.expected
diff --git a/tests/models/records/record2.models.smt2 → tests/models/records/record2.default.smt2 b/tests/models/records/record2.models.smt2 → tests/models/records/record2.default.smt2
diff --git a/tests/models/records/record3.models.expected → ...s/models/records/record3.default.expected b/tests/models/records/record3.models.expected → ...s/models/records/record3.default.expected
diff --git a/tests/models/records/record3.models.smt2 → tests/models/records/record3.default.smt2 b/tests/models/records/record3.models.smt2 → tests/models/records/record3.default.smt2
diff --git a/tests/models/uf/uf1.models.expected → tests/models/uf/uf1.default.expected b/tests/models/uf/uf1.models.expected → tests/models/uf/uf1.default.expected
diff --git a/tests/models/uf/uf1.models.smt2 → tests/models/uf/uf1.default.smt2 b/tests/models/uf/uf1.models.smt2 → tests/models/uf/uf1.default.smt2
diff --git a/tests/models/uf/uf2.models.expected → tests/models/uf/uf2.default.expected b/tests/models/uf/uf2.models.expected → tests/models/uf/uf2.default.expected
diff --git a/tests/models/uf/uf2.models.smt2 → tests/models/uf/uf2.default.smt2 b/tests/models/uf/uf2.models.smt2 → tests/models/uf/uf2.default.smt2
diff --git a/.../dolmen/bitv/bv2nat_bvneg.dolmen.expected → ...iers/testfile-trigger001.default.expected b/.../dolmen/bitv/bv2nat_bvneg.dolmen.expected → ...iers/testfile-trigger001.default.expected
diff --git a/...antifiers/testfile-trigger001.dolmen.smt2 → ...ntifiers/testfile-trigger001.default.smt2 b/...antifiers/testfile-trigger001.dolmen.smt2 → ...ntifiers/testfile-trigger001.default.smt2
diff --git a/tests/quantifiers/testfile-trigger001.dolmen.expected b/tests/quantifiers/testfile-trigger001.dolmen.expected
diff --git a/...quantifiers/testfile-trigger002.dolmen.ae → ...uantifiers/testfile-trigger002.default.ae b/...quantifiers/testfile-trigger002.dolmen.ae → ...uantifiers/testfile-trigger002.default.ae
diff --git a/tests/issues/649/649.dolmen.expected → ...iers/testfile-trigger002.default.expected b/tests/issues/649/649.dolmen.expected → ...iers/testfile-trigger002.default.expected
diff --git a/tests/quantifiers/testfile-trigger002.dolmen.expected b/tests/quantifiers/testfile-trigger002.dolmen.expected
diff --git a/tests/quantifiers/testfile-trigger003.dolmen.expected b/tests/quantifiers/testfile-trigger003.dolmen.expected
diff --git a/tests/quantifiers/testfile-trigger003.dolmen.smt2 b/tests/quantifiers/testfile-trigger003.dolmen.smt2