From 967ac13cb699d5913d45d6c2cfa8daafd71f8ebe Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Tue, 8 Oct 2024 11:01:07 +0200 Subject: [PATCH] Restore tests directory --- .../testfile-array-cs.dolmen.expected} | 0 tests/bitv/testfile-array-cs.dolmen.smt2 | 10 ++++ .../testfile-bv2nat-delayed.dolmen.expected | 2 + .../bitv/testfile-bv2nat-delayed.dolmen.smt2 | 5 ++ .../testfile-bv2nat-immediate.dolmen.expected | 2 + .../testfile-bv2nat-immediate.dolmen.smt2 | 5 ++ .../testfile-bv2nat-models.dolmen.expected | 5 ++ tests/bitv/testfile-bv2nat-models.dolmen.smt2 | 6 ++ tests/bitv/testfile-bvadd-001.dolmen.expected | 2 + tests/bitv/testfile-bvadd-001.dolmen.smt2 | 6 ++ tests/bitv/testfile-bvadd-002.dolmen.expected | 2 + tests/bitv/testfile-bvadd-002.dolmen.smt2 | 8 +++ tests/bitv/testfile-bvand-001.dolmen.expected | 2 + tests/bitv/testfile-bvand-001.dolmen.smt2 | 4 ++ .../testfile-bvnot-term.dolmen.expected} | 0 tests/bitv/testfile-bvnot-term.dolmen.smt2 | 7 +++ ...xpected => testfile-bvnot.dolmen.expected} | 0 ...t.cdcl.smt2 => testfile-bvnot.dolmen.smt2} | 0 tests/bitv/testfile-bvor-001.dolmen.expected | 2 + tests/bitv/testfile-bvor-001.dolmen.smt2 | 4 ++ tests/bitv/testfile-bvsub-001.dolmen.expected | 2 + tests/bitv/testfile-bvsub-001.dolmen.smt2 | 6 ++ tests/bitv/testfile-bvsub-002.dolmen.expected | 2 + tests/bitv/testfile-bvsub-002.dolmen.smt2 | 8 +++ tests/bitv/testfile-bvxor-001.dolmen.expected | 2 + tests/bitv/testfile-bvxor-001.dolmen.smt2 | 4 ++ .../testfile-int2bv-delayed.dolmen.expected | 2 + .../bitv/testfile-int2bv-delayed.dolmen.smt2 | 5 ++ .../testfile-int2bv-immediate.dolmen.expected | 2 + .../testfile-int2bv-immediate.dolmen.smt2 | 5 ++ ...testfile-qfbv-timeout.unix.dolmen.expected | 9 +++ .../testfile-qfbv-timeout.unix.dolmen.smt2 | 58 +++++++++++++++++++ .../bitv/bv2nat_bvneg.dolmen.expected} | 0 tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 | 7 +++ .../dolmen/bitv/bv2nat_bvnot.dolmen.expected | 2 + tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2 | 5 ++ .../bitv/bv2nat_bvnot_range.dolmen.expected | 2 + .../bitv/bv2nat_bvnot_range.dolmen.smt2 | 6 ++ tests/dolmen/bitv/coherence.dolmen.expected | 2 + tests/dolmen/bitv/coherence.dolmen.smt2 | 6 ++ tests/dolmen/bitv/cyclic.dolmen.expected | 2 + tests/dolmen/bitv/cyclic.dolmen.smt2 | 7 +++ tests/dolmen/bitv/not-contra.dolmen.expected | 2 + tests/dolmen/bitv/not-contra.dolmen.smt2 | 7 +++ tests/dolmen/bitv/notextract.dolmen.expected | 2 + tests/dolmen/bitv/notextract.dolmen.smt2 | 8 +++ tests/dolmen/bitv/notnotx.dolmen.expected | 2 + tests/dolmen/bitv/notnotx.dolmen.smt2 | 5 ++ tests/dolmen/bitv/notx.dolmen.expected | 2 + tests/dolmen/bitv/notx.dolmen.smt2 | 5 ++ tests/float/test_float1.dolmen.expected | 2 + tests/float/test_float1.dolmen.smt2 | 6 ++ tests/float/test_float2.models.expected | 5 ++ tests/float/test_float2.models.smt2 | 8 +++ ...163.cdcl.expected => 1163.models.expected} | 0 .../{1163.cdcl.smt2 => 1163.models.smt2} | 0 tests/issues/555.models.expected | 8 +++ tests/issues/555.models.smt2 | 12 ++++ .../649/649.dolmen.expected} | 0 tests/issues/649/649.dolmen.smt2 | 10 ++++ tests/issues/664/664.dolmen.expected | 2 + tests/issues/664/664.dolmen.smt2 | 7 +++ tests/issues/777.models.expected | 5 ++ tests/issues/777.models.smt2 | 7 +++ tests/issues/854/function.models.expected | 8 +++ tests/issues/854/function.models.smt2 | 13 +++++ tests/issues/854/original.models.expected | 7 +++ tests/issues/854/original.models.smt2 | 11 ++++ tests/issues/854/twice_eq.models.expected | 8 +++ tests/issues/854/twice_eq.models.smt2 | 13 +++++ tests/issues/883.dolmen.expected | 2 + tests/issues/883.dolmen.smt2 | 6 ++ tests/issues/926.models.expected | 10 ++++ tests/issues/926.models.smt2 | 16 +++++ ...expected => issue1024.err.dolmen.expected} | 0 ...rr.cdcl.smt2 => issue1024.err.dolmen.smt2} | 0 tests/models/adt/arith.models.expected | 8 +++ tests/models/adt/arith.models.smt2 | 18 ++++++ tests/models/adt/list.models.expected | 8 +++ tests/models/adt/list.models.smt2 | 15 +++++ tests/models/adt/rec.models.expected | 5 ++ tests/models/adt/rec.models.smt2 | 10 ++++ tests/models/adt/rec2.models.expected | 5 ++ tests/models/adt/rec2.models.smt2 | 10 ++++ tests/models/adt/rec3.models.expected | 5 ++ tests/models/adt/rec3.models.smt2 | 10 ++++ tests/models/adt/small.models.expected | 5 ++ tests/models/adt/small.models.smt2 | 11 ++++ tests/models/arith/arith1.models.expected | 5 ++ tests/models/arith/arith1.models.smt2 | 6 ++ ....cdcl.expected => arith10.dolmen.expected} | 0 ...{arith10.cdcl.smt2 => arith10.dolmen.smt2} | 0 ....cdcl.expected => arith11.dolmen.expected} | 0 ...{arith11.cdcl.smt2 => arith11.dolmen.smt2} | 0 ....cdcl.expected => arith12.dolmen.expected} | 0 ...{arith12.cdcl.smt2 => arith12.dolmen.smt2} | 0 ....cdcl.expected => arith13.models.expected} | 0 ...{arith13.cdcl.smt2 => arith13.models.smt2} | 0 ....cdcl.expected => arith14.models.expected} | 0 ...{arith14.cdcl.smt2 => arith14.models.smt2} | 0 ....cdcl.expected => arith15.models.expected} | 0 ...{arith15.cdcl.smt2 => arith15.models.smt2} | 0 tests/models/arith/arith2.models.expected | 6 ++ tests/models/arith/arith2.models.smt2 | 7 +++ ...3.cdcl.expected => arith3.dolmen.expected} | 0 .../{arith3.cdcl.smt2 => arith3.dolmen.smt2} | 0 ...4.cdcl.expected => arith4.dolmen.expected} | 0 .../{arith4.cdcl.smt2 => arith4.dolmen.smt2} | 0 ...5.cdcl.expected => arith5.dolmen.expected} | 0 .../{arith5.cdcl.smt2 => arith5.dolmen.smt2} | 0 ...6.cdcl.expected => arith6.dolmen.expected} | 0 .../{arith6.cdcl.smt2 => arith6.dolmen.smt2} | 0 ...7.cdcl.expected => arith7.dolmen.expected} | 0 .../{arith7.cdcl.smt2 => arith7.dolmen.smt2} | 0 ...8.cdcl.expected => arith8.dolmen.expected} | 0 .../{arith8.cdcl.smt2 => arith8.dolmen.smt2} | 0 ...9.cdcl.expected => arith9.dolmen.expected} | 0 .../{arith9.cdcl.smt2 => arith9.dolmen.smt2} | 0 tests/models/array/array1.models.expected | 8 +++ tests/models/array/array1.models.smt2 | 12 ++++ .../array/embedded-array.models.expected | 8 +++ tests/models/array/embedded-array.models.smt2 | 10 ++++ tests/models/bitv/bvand-1.models.expected | 6 ++ tests/models/bitv/bvand-1.models.smt2 | 9 +++ tests/models/bitv/bvand-2.models.expected | 5 ++ tests/models/bitv/bvand-2.models.smt2 | 6 ++ tests/models/bitv/bvor-1.models.expected | 6 ++ tests/models/bitv/bvor-1.models.smt2 | 9 +++ tests/models/bitv/bvor-2.models.expected | 5 ++ tests/models/bitv/bvor-2.models.smt2 | 6 ++ tests/models/bitv/bvxor-1.models.expected | 6 ++ tests/models/bitv/bvxor-1.models.smt2 | 7 +++ tests/models/bitv/bvxor-2.models.expected | 5 ++ tests/models/bitv/bvxor-2.models.smt2 | 6 ++ tests/models/bitv/cardinal.models.expected | 2 + tests/models/bitv/cardinal.models.smt2 | 11 ++++ .../models/bitv/cs-soundness.models.expected | 5 ++ tests/models/bitv/cs-soundness.models.smt2 | 7 +++ tests/models/bitv/extract.models.expected | 8 +++ tests/models/bitv/extract.models.smt2 | 18 ++++++ tests/models/bitv/manyslice.models.expected | 7 +++ tests/models/bitv/manyslice.models.smt2 | 8 +++ tests/models/bitv/not.models.expected | 5 ++ tests/models/bitv/not.models.smt2 | 7 +++ ....cdcl.expected => optim-1.models.expected} | 0 ...{optim-1.cdcl.smt2 => optim-1.models.smt2} | 0 ....cdcl.expected => optim-2.models.expected} | 0 ...{optim-2.cdcl.smt2 => optim-2.models.smt2} | 0 ....cdcl.expected => optim-3.models.expected} | 0 ...{optim-3.cdcl.smt2 => optim-3.models.smt2} | 0 ....cdcl.expected => optim-4.models.expected} | 0 ...{optim-4.cdcl.smt2 => optim-4.models.smt2} | 0 ....cdcl.expected => optim-5.models.expected} | 0 ...{optim-5.cdcl.smt2 => optim-5.models.smt2} | 0 tests/models/bitv/specified.models.expected | 5 ++ tests/models/bitv/specified.models.smt2 | 10 ++++ tests/models/bool/bool1.models.expected | 18 ++++++ tests/models/bool/bool1.models.smt2 | 16 +++++ ...l2.cdcl.expected => bool2.models.expected} | 0 .../{bool2.cdcl.smt2 => bool2.models.smt2} | 0 tests/models/bool/bool3.models.expected | 9 +++ tests/models/bool/bool3.models.smt2 | 9 +++ tests/models/check_sat.models.ae | 8 +++ tests/models/check_sat.models.expected | 8 +++ ...cl.expected => complete_1.models.expected} | 0 tests/models/complete_1.models.smt2 | 8 +++ tests/models/complete_2.models.expected | 6 ++ tests/models/complete_2.models.smt2 | 8 +++ tests/models/complete_3.models.expected | 5 ++ ...ete_3.cdcl.smt2 => complete_3.models.smt2} | 0 tests/models/issues/715/715_1.models.ae | 6 ++ tests/models/issues/715/715_1.models.expected | 2 + tests/models/issues/715/715_2.models.expected | 5 ++ tests/models/issues/715/715_2.models.smt2 | 8 +++ tests/models/issues/719.models.err.expected | 3 + tests/models/issues/719.models.err.smt2 | 19 ++++++ tests/models/records/record1.models.expected | 5 ++ tests/models/records/record1.models.smt2 | 8 +++ tests/models/records/record2.models.expected | 5 ++ tests/models/records/record2.models.smt2 | 8 +++ tests/models/records/record3.models.expected | 7 +++ tests/models/records/record3.models.smt2 | 12 ++++ tests/models/uf/uf1.models.expected | 7 +++ tests/models/uf/uf1.models.smt2 | 8 +++ tests/models/uf/uf2.models.expected | 7 +++ tests/models/uf/uf2.models.smt2 | 8 +++ .../testfile-trigger001.dolmen.expected | 2 + ...l.smt2 => testfile-trigger001.dolmen.smt2} | 0 ....cdcl.ae => testfile-trigger002.dolmen.ae} | 0 .../testfile-trigger002.dolmen.expected | 2 + .../testfile-trigger003.dolmen.expected | 2 + .../testfile-trigger003.dolmen.smt2 | 16 +++++ .../quantifiers/testfile-trigger004.dolmen.ae | 11 ++++ .../testfile-trigger004.dolmen.expected | 2 + ...clare-datatype-incremental.dolmen.expected | 2 + ...-declare-datatype-incremental.dolmen.smt2} | 0 tests/smtlib/testfile-echo1.dolmen.expected | 1 + tests/smtlib/testfile-echo1.dolmen.smt2 | 2 + tests/smtlib/testfile-echo2.dolmen.expected | 1 + tests/smtlib/testfile-echo2.dolmen.smt2 | 2 + tests/smtlib/testfile-exit.dolmen.expected | 2 + tests/smtlib/testfile-exit.dolmen.smt2 | 4 ++ ...stfile-get-assignment1.err.dolmen.expected | 1 + .../testfile-get-assignment1.err.dolmen.smt2 | 3 + ...stfile-get-assignment2.err.dolmen.expected | 6 ++ .../testfile-get-assignment2.err.dolmen.smt2 | 8 +++ .../testfile-get-assignment3.dolmen.expected | 4 ++ .../testfile-get-assignment3.dolmen.smt2 | 6 ++ ...ted => testfile-get-info1.dolmen.expected} | 0 ...cl.smt2 => testfile-get-info1.dolmen.smt2} | 0 .../testfile-get-info2.err.dolmen.expected | 1 + .../smtlib/testfile-get-info2.err.dolmen.smt2 | 8 +++ .../smtlib/testfile-get-info3.dolmen.expected | 1 + tests/smtlib/testfile-get-info3.dolmen.smt2 | 1 + ...=> testfile-push-pop1.err.dolmen.expected} | 0 ...mt2 => testfile-push-pop1.err.dolmen.smt2} | 0 .../smtlib/testfile-push-pop2.dolmen.expected | 2 + ...cl.smt2 => testfile-push-pop2.dolmen.smt2} | 0 tests/smtlib/testfile-quoted1.dolmen.expected | 5 ++ tests/smtlib/testfile-quoted1.dolmen.smt2 | 6 ++ tests/smtlib/testfile-reset.dolmen.expected | 4 ++ tests/smtlib/testfile-reset.dolmen.smt2 | 8 +++ .../testfile-steps-bound1.dolmen.err.expected | 1 + .../testfile-steps-bound1.dolmen.err.smt2 | 7 +++ ... => testfile-steps-bound2.dolmen.expected} | 0 ...smt2 => testfile-steps-bound2.dolmen.smt2} | 0 226 files changed, 1090 insertions(+) rename tests/{smtlib/testfile-declare-datatype-incremental.cdcl.expected => bitv/testfile-array-cs.dolmen.expected} (100%) create mode 100644 tests/bitv/testfile-array-cs.dolmen.smt2 create mode 100644 tests/bitv/testfile-bv2nat-delayed.dolmen.expected create mode 100644 tests/bitv/testfile-bv2nat-delayed.dolmen.smt2 create mode 100644 tests/bitv/testfile-bv2nat-immediate.dolmen.expected create mode 100644 tests/bitv/testfile-bv2nat-immediate.dolmen.smt2 create mode 100644 tests/bitv/testfile-bv2nat-models.dolmen.expected create mode 100644 tests/bitv/testfile-bv2nat-models.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvadd-001.dolmen.expected create mode 100644 tests/bitv/testfile-bvadd-001.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvadd-002.dolmen.expected create mode 100644 tests/bitv/testfile-bvadd-002.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvand-001.dolmen.expected create mode 100644 tests/bitv/testfile-bvand-001.dolmen.smt2 rename tests/{quantifiers/testfile-trigger001.cdcl.expected => bitv/testfile-bvnot-term.dolmen.expected} (100%) create mode 100644 tests/bitv/testfile-bvnot-term.dolmen.smt2 rename tests/bitv/{testfile-bvnot.cdcl.expected => testfile-bvnot.dolmen.expected} (100%) rename tests/bitv/{testfile-bvnot.cdcl.smt2 => testfile-bvnot.dolmen.smt2} (100%) create mode 100644 tests/bitv/testfile-bvor-001.dolmen.expected create mode 100644 tests/bitv/testfile-bvor-001.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvsub-001.dolmen.expected create mode 100644 tests/bitv/testfile-bvsub-001.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvsub-002.dolmen.expected create mode 100644 tests/bitv/testfile-bvsub-002.dolmen.smt2 create mode 100644 tests/bitv/testfile-bvxor-001.dolmen.expected create mode 100644 tests/bitv/testfile-bvxor-001.dolmen.smt2 create mode 100644 tests/bitv/testfile-int2bv-delayed.dolmen.expected create mode 100644 tests/bitv/testfile-int2bv-delayed.dolmen.smt2 create mode 100644 tests/bitv/testfile-int2bv-immediate.dolmen.expected create mode 100644 tests/bitv/testfile-int2bv-immediate.dolmen.smt2 create mode 100644 tests/bitv/testfile-qfbv-timeout.unix.dolmen.expected create mode 100644 tests/bitv/testfile-qfbv-timeout.unix.dolmen.smt2 rename tests/{quantifiers/testfile-trigger002.cdcl.expected => dolmen/bitv/bv2nat_bvneg.dolmen.expected} (100%) create mode 100644 tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 create mode 100644 tests/dolmen/bitv/bv2nat_bvnot.dolmen.expected create mode 100644 tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2 create mode 100644 tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.expected create mode 100644 tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.smt2 create mode 100644 tests/dolmen/bitv/coherence.dolmen.expected create mode 100644 tests/dolmen/bitv/coherence.dolmen.smt2 create mode 100644 tests/dolmen/bitv/cyclic.dolmen.expected create mode 100644 tests/dolmen/bitv/cyclic.dolmen.smt2 create mode 100644 tests/dolmen/bitv/not-contra.dolmen.expected create mode 100644 tests/dolmen/bitv/not-contra.dolmen.smt2 create mode 100644 tests/dolmen/bitv/notextract.dolmen.expected create mode 100644 tests/dolmen/bitv/notextract.dolmen.smt2 create mode 100644 tests/dolmen/bitv/notnotx.dolmen.expected create mode 100644 tests/dolmen/bitv/notnotx.dolmen.smt2 create mode 100644 tests/dolmen/bitv/notx.dolmen.expected create mode 100644 tests/dolmen/bitv/notx.dolmen.smt2 create mode 100644 tests/float/test_float1.dolmen.expected create mode 100644 tests/float/test_float1.dolmen.smt2 create mode 100644 tests/float/test_float2.models.expected create mode 100644 tests/float/test_float2.models.smt2 rename tests/issues/{1163.cdcl.expected => 1163.models.expected} (100%) rename tests/issues/{1163.cdcl.smt2 => 1163.models.smt2} (100%) create mode 100644 tests/issues/555.models.expected create mode 100644 tests/issues/555.models.smt2 rename tests/{smtlib/testfile-push-pop2.cdcl.expected => issues/649/649.dolmen.expected} (100%) create mode 100644 tests/issues/649/649.dolmen.smt2 create mode 100644 tests/issues/664/664.dolmen.expected create mode 100644 tests/issues/664/664.dolmen.smt2 create mode 100644 tests/issues/777.models.expected create mode 100644 tests/issues/777.models.smt2 create mode 100644 tests/issues/854/function.models.expected create mode 100644 tests/issues/854/function.models.smt2 create mode 100644 tests/issues/854/original.models.expected create mode 100644 tests/issues/854/original.models.smt2 create mode 100644 tests/issues/854/twice_eq.models.expected create mode 100644 tests/issues/854/twice_eq.models.smt2 create mode 100644 tests/issues/883.dolmen.expected create mode 100644 tests/issues/883.dolmen.smt2 create mode 100644 tests/issues/926.models.expected create mode 100644 tests/issues/926.models.smt2 rename tests/issues/{1024.err.cdcl.expected => issue1024.err.dolmen.expected} (100%) rename tests/issues/{1024.err.cdcl.smt2 => issue1024.err.dolmen.smt2} (100%) create mode 100644 tests/models/adt/arith.models.expected create mode 100644 tests/models/adt/arith.models.smt2 create mode 100644 tests/models/adt/list.models.expected create mode 100644 tests/models/adt/list.models.smt2 create mode 100644 tests/models/adt/rec.models.expected create mode 100644 tests/models/adt/rec.models.smt2 create mode 100644 tests/models/adt/rec2.models.expected create mode 100644 tests/models/adt/rec2.models.smt2 create mode 100644 tests/models/adt/rec3.models.expected create mode 100644 tests/models/adt/rec3.models.smt2 create mode 100644 tests/models/adt/small.models.expected create mode 100644 tests/models/adt/small.models.smt2 create mode 100644 tests/models/arith/arith1.models.expected create mode 100644 tests/models/arith/arith1.models.smt2 rename tests/models/arith/{arith10.cdcl.expected => arith10.dolmen.expected} (100%) rename tests/models/arith/{arith10.cdcl.smt2 => arith10.dolmen.smt2} (100%) rename tests/models/arith/{arith11.cdcl.expected => arith11.dolmen.expected} (100%) rename tests/models/arith/{arith11.cdcl.smt2 => arith11.dolmen.smt2} (100%) rename tests/models/arith/{arith12.cdcl.expected => arith12.dolmen.expected} (100%) rename tests/models/arith/{arith12.cdcl.smt2 => arith12.dolmen.smt2} (100%) rename tests/models/arith/{arith13.cdcl.expected => arith13.models.expected} (100%) rename tests/models/arith/{arith13.cdcl.smt2 => arith13.models.smt2} (100%) rename tests/models/arith/{arith14.cdcl.expected => arith14.models.expected} (100%) rename tests/models/arith/{arith14.cdcl.smt2 => arith14.models.smt2} (100%) rename tests/models/arith/{arith15.cdcl.expected => arith15.models.expected} (100%) rename tests/models/arith/{arith15.cdcl.smt2 => arith15.models.smt2} (100%) create mode 100644 tests/models/arith/arith2.models.expected create mode 100644 tests/models/arith/arith2.models.smt2 rename tests/models/arith/{arith3.cdcl.expected => arith3.dolmen.expected} (100%) rename tests/models/arith/{arith3.cdcl.smt2 => arith3.dolmen.smt2} (100%) rename tests/models/arith/{arith4.cdcl.expected => arith4.dolmen.expected} (100%) rename tests/models/arith/{arith4.cdcl.smt2 => arith4.dolmen.smt2} (100%) rename tests/models/arith/{arith5.cdcl.expected => arith5.dolmen.expected} (100%) rename tests/models/arith/{arith5.cdcl.smt2 => arith5.dolmen.smt2} (100%) rename tests/models/arith/{arith6.cdcl.expected => arith6.dolmen.expected} (100%) rename tests/models/arith/{arith6.cdcl.smt2 => arith6.dolmen.smt2} (100%) rename tests/models/arith/{arith7.cdcl.expected => arith7.dolmen.expected} (100%) rename tests/models/arith/{arith7.cdcl.smt2 => arith7.dolmen.smt2} (100%) rename tests/models/arith/{arith8.cdcl.expected => arith8.dolmen.expected} (100%) rename tests/models/arith/{arith8.cdcl.smt2 => arith8.dolmen.smt2} (100%) rename tests/models/arith/{arith9.cdcl.expected => arith9.dolmen.expected} (100%) rename tests/models/arith/{arith9.cdcl.smt2 => arith9.dolmen.smt2} (100%) create mode 100644 tests/models/array/array1.models.expected create mode 100644 tests/models/array/array1.models.smt2 create mode 100644 tests/models/array/embedded-array.models.expected create mode 100644 tests/models/array/embedded-array.models.smt2 create mode 100644 tests/models/bitv/bvand-1.models.expected create mode 100644 tests/models/bitv/bvand-1.models.smt2 create mode 100644 tests/models/bitv/bvand-2.models.expected create mode 100644 tests/models/bitv/bvand-2.models.smt2 create mode 100644 tests/models/bitv/bvor-1.models.expected create mode 100644 tests/models/bitv/bvor-1.models.smt2 create mode 100644 tests/models/bitv/bvor-2.models.expected create mode 100644 tests/models/bitv/bvor-2.models.smt2 create mode 100644 tests/models/bitv/bvxor-1.models.expected create mode 100644 tests/models/bitv/bvxor-1.models.smt2 create mode 100644 tests/models/bitv/bvxor-2.models.expected create mode 100644 tests/models/bitv/bvxor-2.models.smt2 create mode 100644 tests/models/bitv/cardinal.models.expected create mode 100644 tests/models/bitv/cardinal.models.smt2 create mode 100644 tests/models/bitv/cs-soundness.models.expected create mode 100644 tests/models/bitv/cs-soundness.models.smt2 create mode 100644 tests/models/bitv/extract.models.expected create mode 100644 tests/models/bitv/extract.models.smt2 create mode 100644 tests/models/bitv/manyslice.models.expected create mode 100644 tests/models/bitv/manyslice.models.smt2 create mode 100644 tests/models/bitv/not.models.expected create mode 100644 tests/models/bitv/not.models.smt2 rename tests/models/bitv/{optim-1.cdcl.expected => optim-1.models.expected} (100%) rename tests/models/bitv/{optim-1.cdcl.smt2 => optim-1.models.smt2} (100%) rename tests/models/bitv/{optim-2.cdcl.expected => optim-2.models.expected} (100%) rename tests/models/bitv/{optim-2.cdcl.smt2 => optim-2.models.smt2} (100%) rename tests/models/bitv/{optim-3.cdcl.expected => optim-3.models.expected} (100%) rename tests/models/bitv/{optim-3.cdcl.smt2 => optim-3.models.smt2} (100%) rename tests/models/bitv/{optim-4.cdcl.expected => optim-4.models.expected} (100%) rename tests/models/bitv/{optim-4.cdcl.smt2 => optim-4.models.smt2} (100%) rename tests/models/bitv/{optim-5.cdcl.expected => optim-5.models.expected} (100%) rename tests/models/bitv/{optim-5.cdcl.smt2 => optim-5.models.smt2} (100%) create mode 100644 tests/models/bitv/specified.models.expected create mode 100644 tests/models/bitv/specified.models.smt2 create mode 100644 tests/models/bool/bool1.models.expected create mode 100644 tests/models/bool/bool1.models.smt2 rename tests/models/bool/{bool2.cdcl.expected => bool2.models.expected} (100%) rename tests/models/bool/{bool2.cdcl.smt2 => bool2.models.smt2} (100%) create mode 100644 tests/models/bool/bool3.models.expected create mode 100644 tests/models/bool/bool3.models.smt2 create mode 100644 tests/models/check_sat.models.ae create mode 100644 tests/models/check_sat.models.expected rename tests/models/{complete_3.cdcl.expected => complete_1.models.expected} (100%) create mode 100644 tests/models/complete_1.models.smt2 create mode 100644 tests/models/complete_2.models.expected create mode 100644 tests/models/complete_2.models.smt2 create mode 100644 tests/models/complete_3.models.expected rename tests/models/{complete_3.cdcl.smt2 => complete_3.models.smt2} (100%) create mode 100644 tests/models/issues/715/715_1.models.ae create mode 100644 tests/models/issues/715/715_1.models.expected create mode 100644 tests/models/issues/715/715_2.models.expected create mode 100644 tests/models/issues/715/715_2.models.smt2 create mode 100644 tests/models/issues/719.models.err.expected create mode 100644 tests/models/issues/719.models.err.smt2 create mode 100644 tests/models/records/record1.models.expected create mode 100644 tests/models/records/record1.models.smt2 create mode 100644 tests/models/records/record2.models.expected create mode 100644 tests/models/records/record2.models.smt2 create mode 100644 tests/models/records/record3.models.expected create mode 100644 tests/models/records/record3.models.smt2 create mode 100644 tests/models/uf/uf1.models.expected create mode 100644 tests/models/uf/uf1.models.smt2 create mode 100644 tests/models/uf/uf2.models.expected create mode 100644 tests/models/uf/uf2.models.smt2 create mode 100644 tests/quantifiers/testfile-trigger001.dolmen.expected rename tests/quantifiers/{testfile-trigger001.cdcl.smt2 => testfile-trigger001.dolmen.smt2} (100%) rename tests/quantifiers/{testfile-trigger002.cdcl.ae => testfile-trigger002.dolmen.ae} (100%) create mode 100644 tests/quantifiers/testfile-trigger002.dolmen.expected create mode 100644 tests/quantifiers/testfile-trigger003.dolmen.expected create mode 100644 tests/quantifiers/testfile-trigger003.dolmen.smt2 create mode 100644 tests/quantifiers/testfile-trigger004.dolmen.ae create mode 100644 tests/quantifiers/testfile-trigger004.dolmen.expected create mode 100644 tests/smtlib/testfile-declare-datatype-incremental.dolmen.expected rename tests/smtlib/{testfile-declare-datatype-incremental.cdcl.smt2 => testfile-declare-datatype-incremental.dolmen.smt2} (100%) create mode 100644 tests/smtlib/testfile-echo1.dolmen.expected create mode 100644 tests/smtlib/testfile-echo1.dolmen.smt2 create mode 100644 tests/smtlib/testfile-echo2.dolmen.expected create mode 100644 tests/smtlib/testfile-echo2.dolmen.smt2 create mode 100644 tests/smtlib/testfile-exit.dolmen.expected create mode 100644 tests/smtlib/testfile-exit.dolmen.smt2 create mode 100644 tests/smtlib/testfile-get-assignment1.err.dolmen.expected create mode 100644 tests/smtlib/testfile-get-assignment1.err.dolmen.smt2 create mode 100644 tests/smtlib/testfile-get-assignment2.err.dolmen.expected create mode 100644 tests/smtlib/testfile-get-assignment2.err.dolmen.smt2 create mode 100644 tests/smtlib/testfile-get-assignment3.dolmen.expected create mode 100644 tests/smtlib/testfile-get-assignment3.dolmen.smt2 rename tests/smtlib/{testfile-get-info1.cdcl.expected => testfile-get-info1.dolmen.expected} (100%) rename tests/smtlib/{testfile-get-info1.cdcl.smt2 => testfile-get-info1.dolmen.smt2} (100%) create mode 100644 tests/smtlib/testfile-get-info2.err.dolmen.expected create mode 100644 tests/smtlib/testfile-get-info2.err.dolmen.smt2 create mode 100644 tests/smtlib/testfile-get-info3.dolmen.expected create mode 100644 tests/smtlib/testfile-get-info3.dolmen.smt2 rename tests/smtlib/{testfile-push-pop1.err.cdcl.expected => testfile-push-pop1.err.dolmen.expected} (100%) rename tests/smtlib/{testfile-push-pop1.err.cdcl.smt2 => testfile-push-pop1.err.dolmen.smt2} (100%) create mode 100644 tests/smtlib/testfile-push-pop2.dolmen.expected rename tests/smtlib/{testfile-push-pop2.cdcl.smt2 => testfile-push-pop2.dolmen.smt2} (100%) create mode 100644 tests/smtlib/testfile-quoted1.dolmen.expected create mode 100644 tests/smtlib/testfile-quoted1.dolmen.smt2 create mode 100644 tests/smtlib/testfile-reset.dolmen.expected create mode 100644 tests/smtlib/testfile-reset.dolmen.smt2 create mode 100644 tests/smtlib/testfile-steps-bound1.dolmen.err.expected create mode 100644 tests/smtlib/testfile-steps-bound1.dolmen.err.smt2 rename tests/smtlib/{testfile-steps-bound2.cdcl.expected => testfile-steps-bound2.dolmen.expected} (100%) rename tests/smtlib/{testfile-steps-bound2.cdcl.smt2 => testfile-steps-bound2.dolmen.smt2} (100%) diff --git a/tests/smtlib/testfile-declare-datatype-incremental.cdcl.expected b/tests/bitv/testfile-array-cs.dolmen.expected similarity index 100% rename from tests/smtlib/testfile-declare-datatype-incremental.cdcl.expected rename to tests/bitv/testfile-array-cs.dolmen.expected diff --git a/tests/bitv/testfile-array-cs.dolmen.smt2 b/tests/bitv/testfile-array-cs.dolmen.smt2 new file mode 100644 index 000000000..8ad600952 --- /dev/null +++ b/tests/bitv/testfile-array-cs.dolmen.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +; We need produce-models to propagate `int2bv` when learning `0 = y` +(set-option :produce-models true) +(declare-const a (Array Int Int)) +(declare-const x Int) +(declare-const y Int) +(assert (= (select a 4) 1)) +(assert (= (select (store a y 0) 4) 0)) +(assert (= ((_ int2bv 2) y) #b11)) +(check-sat) diff --git a/tests/bitv/testfile-bv2nat-delayed.dolmen.expected b/tests/bitv/testfile-bv2nat-delayed.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bv2nat-delayed.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bv2nat-delayed.dolmen.smt2 b/tests/bitv/testfile-bv2nat-delayed.dolmen.smt2 new file mode 100644 index 000000000..463832ae2 --- /dev/null +++ b/tests/bitv/testfile-bv2nat-delayed.dolmen.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(declare-const x (_ BitVec 32)) +(assert (distinct (bv2nat x) 2)) +(assert (= x #b00000000000000000000000000000010)) +(check-sat) diff --git a/tests/bitv/testfile-bv2nat-immediate.dolmen.expected b/tests/bitv/testfile-bv2nat-immediate.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bv2nat-immediate.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bv2nat-immediate.dolmen.smt2 b/tests/bitv/testfile-bv2nat-immediate.dolmen.smt2 new file mode 100644 index 000000000..467c210cc --- /dev/null +++ b/tests/bitv/testfile-bv2nat-immediate.dolmen.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(declare-const x (_ BitVec 32)) +(assert (= x #b00000000000000000000000000000010)) +(assert (distinct (bv2nat x) 2)) +(check-sat) diff --git a/tests/bitv/testfile-bv2nat-models.dolmen.expected b/tests/bitv/testfile-bv2nat-models.dolmen.expected new file mode 100644 index 000000000..c79ed8694 --- /dev/null +++ b/tests/bitv/testfile-bv2nat-models.dolmen.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () (_ BitVec 4) #x7) +) diff --git a/tests/bitv/testfile-bv2nat-models.dolmen.smt2 b/tests/bitv/testfile-bv2nat-models.dolmen.smt2 new file mode 100644 index 000000000..459ea52d7 --- /dev/null +++ b/tests/bitv/testfile-bv2nat-models.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x (_ BitVec 4)) +(assert (= (bv2nat x) 7)) +(check-sat) +(get-model) diff --git a/tests/bitv/testfile-bvadd-001.dolmen.expected b/tests/bitv/testfile-bvadd-001.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvadd-001.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvadd-001.dolmen.smt2 b/tests/bitv/testfile-bvadd-001.dolmen.smt2 new file mode 100644 index 000000000..6a5a3b878 --- /dev/null +++ b/tests/bitv/testfile-bvadd-001.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(declare-const x (_ BitVec 1024)) +(declare-const y (_ BitVec 1024)) +; Addition of low bits is independent from high bits +(assert (distinct ((_ extract 3 0) (bvadd (concat x #b0101) (concat y #b1100))) #b0001)) +(check-sat) diff --git a/tests/bitv/testfile-bvadd-002.dolmen.expected b/tests/bitv/testfile-bvadd-002.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvadd-002.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvadd-002.dolmen.smt2 b/tests/bitv/testfile-bvadd-002.dolmen.smt2 new file mode 100644 index 000000000..7438211f6 --- /dev/null +++ b/tests/bitv/testfile-bvadd-002.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(declare-const x (_ BitVec 1024)) +(declare-const y (_ BitVec 1024)) +(declare-const z (_ BitVec 1024)) +(declare-const w (_ BitVec 1024)) +; Double zero stops carries +(assert (distinct ((_ extract 1027 1025) (bvadd (concat x (concat #b0100 y)) (concat y (concat #b1100 z)))) #b000)) +(check-sat) diff --git a/tests/bitv/testfile-bvand-001.dolmen.expected b/tests/bitv/testfile-bvand-001.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvand-001.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvand-001.dolmen.smt2 b/tests/bitv/testfile-bvand-001.dolmen.smt2 new file mode 100644 index 000000000..1bdf90b97 --- /dev/null +++ b/tests/bitv/testfile-bvand-001.dolmen.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(declare-const x (_ BitVec 8)) +(assert (distinct #b00000000 (bvand x (bvnot x)))) +(check-sat) diff --git a/tests/quantifiers/testfile-trigger001.cdcl.expected b/tests/bitv/testfile-bvnot-term.dolmen.expected similarity index 100% rename from tests/quantifiers/testfile-trigger001.cdcl.expected rename to tests/bitv/testfile-bvnot-term.dolmen.expected diff --git a/tests/bitv/testfile-bvnot-term.dolmen.smt2 b/tests/bitv/testfile-bvnot-term.dolmen.smt2 new file mode 100644 index 000000000..fe478a577 --- /dev/null +++ b/tests/bitv/testfile-bvnot-term.dolmen.smt2 @@ -0,0 +1,7 @@ +(set-logic BV) + +(declare-const x (_ BitVec 4)) +(declare-const y (_ BitVec 4)) +(assert (= x (bvnot y))) +(assert (distinct y x)) +(check-sat) diff --git a/tests/bitv/testfile-bvnot.cdcl.expected b/tests/bitv/testfile-bvnot.dolmen.expected similarity index 100% rename from tests/bitv/testfile-bvnot.cdcl.expected rename to tests/bitv/testfile-bvnot.dolmen.expected diff --git a/tests/bitv/testfile-bvnot.cdcl.smt2 b/tests/bitv/testfile-bvnot.dolmen.smt2 similarity index 100% rename from tests/bitv/testfile-bvnot.cdcl.smt2 rename to tests/bitv/testfile-bvnot.dolmen.smt2 diff --git a/tests/bitv/testfile-bvor-001.dolmen.expected b/tests/bitv/testfile-bvor-001.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvor-001.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvor-001.dolmen.smt2 b/tests/bitv/testfile-bvor-001.dolmen.smt2 new file mode 100644 index 000000000..02edaffd5 --- /dev/null +++ b/tests/bitv/testfile-bvor-001.dolmen.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(declare-const x (_ BitVec 8)) +(assert (distinct #b11111111 (bvor x (bvnot x)))) +(check-sat) diff --git a/tests/bitv/testfile-bvsub-001.dolmen.expected b/tests/bitv/testfile-bvsub-001.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvsub-001.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvsub-001.dolmen.smt2 b/tests/bitv/testfile-bvsub-001.dolmen.smt2 new file mode 100644 index 000000000..4848ce195 --- /dev/null +++ b/tests/bitv/testfile-bvsub-001.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(declare-const x (_ BitVec 1024)) +(declare-const y (_ BitVec 1024)) +; Subtraction of low bits is independent of high bits +(assert (distinct ((_ extract 3 0) (bvsub (concat x #b0101) (concat y #b0111))) #b1110)) +(check-sat) diff --git a/tests/bitv/testfile-bvsub-002.dolmen.expected b/tests/bitv/testfile-bvsub-002.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvsub-002.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvsub-002.dolmen.smt2 b/tests/bitv/testfile-bvsub-002.dolmen.smt2 new file mode 100644 index 000000000..a6636eae2 --- /dev/null +++ b/tests/bitv/testfile-bvsub-002.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(declare-const x (_ BitVec 1024)) +(declare-const y (_ BitVec 1024)) +(declare-const z (_ BitVec 1024)) +(declare-const w (_ BitVec 1024)) +; Double zero stops carries +(assert (distinct ((_ extract 1027 1025) (bvsub (concat x (concat #b0101 y)) (concat y (concat #b0100 z)))) #b000)) +(check-sat) diff --git a/tests/bitv/testfile-bvxor-001.dolmen.expected b/tests/bitv/testfile-bvxor-001.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-bvxor-001.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-bvxor-001.dolmen.smt2 b/tests/bitv/testfile-bvxor-001.dolmen.smt2 new file mode 100644 index 000000000..f2d7a01f7 --- /dev/null +++ b/tests/bitv/testfile-bvxor-001.dolmen.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(declare-const x (_ BitVec 8)) +(assert (= x (bvxor #b10100101 x))) +(check-sat) diff --git a/tests/bitv/testfile-int2bv-delayed.dolmen.expected b/tests/bitv/testfile-int2bv-delayed.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-int2bv-delayed.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-int2bv-delayed.dolmen.smt2 b/tests/bitv/testfile-int2bv-delayed.dolmen.smt2 new file mode 100644 index 000000000..347264770 --- /dev/null +++ b/tests/bitv/testfile-int2bv-delayed.dolmen.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(declare-const x Int) +(assert (distinct ((_ int2bv 4) x) #b0101)) +(assert (= x 5)) +(check-sat) diff --git a/tests/bitv/testfile-int2bv-immediate.dolmen.expected b/tests/bitv/testfile-int2bv-immediate.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/bitv/testfile-int2bv-immediate.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/bitv/testfile-int2bv-immediate.dolmen.smt2 b/tests/bitv/testfile-int2bv-immediate.dolmen.smt2 new file mode 100644 index 000000000..6abca1303 --- /dev/null +++ b/tests/bitv/testfile-int2bv-immediate.dolmen.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(declare-const x Int) +(assert (= x 5)) +(assert (distinct ((_ int2bv 4) x) #b0101)) +(check-sat) diff --git a/tests/bitv/testfile-qfbv-timeout.unix.dolmen.expected b/tests/bitv/testfile-qfbv-timeout.unix.dolmen.expected new file mode 100644 index 000000000..3c63839ab --- /dev/null +++ b/tests/bitv/testfile-qfbv-timeout.unix.dolmen.expected @@ -0,0 +1,9 @@ + +unknown +(:reason-unknown (:timeout :assume)) + +unknown +(:reason-unknown (:timeout :assume)) + +unknown +(:reason-unknown (:timeout :assume)) diff --git a/tests/bitv/testfile-qfbv-timeout.unix.dolmen.smt2 b/tests/bitv/testfile-qfbv-timeout.unix.dolmen.smt2 new file mode 100644 index 000000000..27fcf0299 --- /dev/null +++ b/tests/bitv/testfile-qfbv-timeout.unix.dolmen.smt2 @@ -0,0 +1,58 @@ +(set-info :smt-lib-version 2.6) +(set-option :reproducible-resource-limit 1) +(set-logic QF_BV) +(set-info :source | + Patrice Godefroid, SAGE (systematic dynamic test generation) + For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf +|) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun T4_11167 () (_ BitVec 32)) +(declare-fun T2_10410 () (_ BitVec 16)) +(declare-fun T2_10408 () (_ BitVec 16)) +(declare-fun T2_10475 () (_ BitVec 16)) +(declare-fun T2_10473 () (_ BitVec 16)) +(declare-fun T2_10532 () (_ BitVec 16)) +(declare-fun T2_10530 () (_ BitVec 16)) +(declare-fun T2_10606 () (_ BitVec 16)) +(declare-fun T2_10604 () (_ BitVec 16)) +(declare-fun T2_10669 () (_ BitVec 16)) +(declare-fun T2_10667 () (_ BitVec 16)) +(declare-fun T2_10734 () (_ BitVec 16)) +(declare-fun T2_10736 () (_ BitVec 16)) +(declare-fun T1_11167 () (_ BitVec 8)) +(declare-fun T1_11168 () (_ BitVec 8)) +(declare-fun T1_11169 () (_ BitVec 8)) +(declare-fun T1_11170 () (_ BitVec 8)) +(declare-fun T1_10736 () (_ BitVec 8)) +(declare-fun T1_10737 () (_ BitVec 8)) +(declare-fun T1_10734 () (_ BitVec 8)) +(declare-fun T1_10735 () (_ BitVec 8)) +(declare-fun T1_10669 () (_ BitVec 8)) +(declare-fun T1_10670 () (_ BitVec 8)) +(declare-fun T1_10667 () (_ BitVec 8)) +(declare-fun T1_10668 () (_ BitVec 8)) +(declare-fun T1_10606 () (_ BitVec 8)) +(declare-fun T1_10607 () (_ BitVec 8)) +(declare-fun T1_10604 () (_ BitVec 8)) +(declare-fun T1_10605 () (_ BitVec 8)) +(declare-fun T1_10532 () (_ BitVec 8)) +(declare-fun T1_10533 () (_ BitVec 8)) +(declare-fun T1_10530 () (_ BitVec 8)) +(declare-fun T1_10531 () (_ BitVec 8)) +(declare-fun T1_10475 () (_ BitVec 8)) +(declare-fun T1_10476 () (_ BitVec 8)) +(declare-fun T1_10473 () (_ BitVec 8)) +(declare-fun T1_10474 () (_ BitVec 8)) +(declare-fun T1_10410 () (_ BitVec 8)) +(declare-fun T1_10411 () (_ BitVec 8)) +(declare-fun T1_10408 () (_ BitVec 8)) +(declare-fun T1_10409 () (_ BitVec 8)) +(assert (let ((?v_0 (bvadd T4_11167 (_ bv4 32))) (?v_12 ((_ zero_extend 16) T2_10408))) (let ((?v_10 (bvadd ?v_0 (bvsub (bvadd (bvadd (bvadd ?v_0 (_ bv61 32)) ?v_12) ((_ zero_extend 16) T2_10410)) ?v_0)))) (let ((?v_1 (bvadd ?v_10 (_ bv4 32))) (?v_18 ((_ zero_extend 16) T2_10473))) (let ((?v_16 (bvadd ?v_1 (bvsub (bvadd (bvadd (bvadd ?v_1 (_ bv53 32)) ?v_18) ((_ zero_extend 16) T2_10475)) ?v_1)))) (let ((?v_2 (bvadd ?v_16 (_ bv4 32))) (?v_24 ((_ zero_extend 16) T2_10530))) (let ((?v_22 (bvadd ?v_2 (bvsub (bvadd (bvadd (bvadd ?v_2 (_ bv70 32)) ?v_24) ((_ zero_extend 16) T2_10532)) ?v_2)))) (let ((?v_3 (bvadd ?v_22 (_ bv4 32))) (?v_30 ((_ zero_extend 16) T2_10604))) (let ((?v_28 (bvadd ?v_3 (bvsub (bvadd (bvadd (bvadd ?v_3 (_ bv59 32)) ?v_30) ((_ zero_extend 16) T2_10606)) ?v_3)))) (let ((?v_4 (bvadd ?v_28 (_ bv4 32))) (?v_36 ((_ zero_extend 16) T2_10667))) (let ((?v_34 (bvadd ?v_4 (bvsub (bvadd (bvadd (bvadd ?v_4 (_ bv63 32)) ?v_36) ((_ zero_extend 16) T2_10669)) ?v_4)))) (let ((?v_5 (bvadd ?v_34 (_ bv4 32)))) (let ((?v_40 (bvadd ?v_5 (_ bv42 32))) (?v_39 ((_ zero_extend 16) T2_10734)) (?v_38 (bvadd ?v_4 (_ bv42 32))) (?v_37 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_5) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_35 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_34) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_33 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_40) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_32 (bvadd ?v_3 (_ bv42 32))) (?v_31 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_4) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_29 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_28) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_27 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_38) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_26 (bvadd ?v_2 (_ bv42 32))) (?v_25 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_3) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_23 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_22) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_21 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_32) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_20 (bvadd ?v_1 (_ bv42 32))) (?v_19 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_2) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_17 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_16) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_15 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_26) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_14 (bvadd ?v_0 (_ bv42 32))) (?v_13 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_1) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_11 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_10) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (let ((?v_9 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_20) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_8 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_0) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_7 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) T4_11167) (_ bv0 32)) (_ bv1 8) (_ bv0 8))))) (?v_6 (bvsub (_ bv4294967295 32) ((_ zero_extend 24) (ite (bvult (bvsub (_ bv4294967295 32) ?v_14) (_ bv0 32)) (_ bv1 8) (_ bv0 8)))))) (and true (= T2_10408 (bvor (bvshl ((_ zero_extend 8) T1_10409) (_ bv8 16)) ((_ zero_extend 8) T1_10408))) (= T2_10410 (bvor (bvshl ((_ zero_extend 8) T1_10411) (_ bv8 16)) ((_ zero_extend 8) T1_10410))) (= T2_10473 (bvor (bvshl ((_ zero_extend 8) T1_10474) (_ bv8 16)) ((_ zero_extend 8) T1_10473))) (= T2_10475 (bvor (bvshl ((_ zero_extend 8) T1_10476) (_ bv8 16)) ((_ zero_extend 8) T1_10475))) (= T2_10530 (bvor (bvshl ((_ zero_extend 8) T1_10531) (_ bv8 16)) ((_ zero_extend 8) T1_10530))) (= T2_10532 (bvor (bvshl ((_ zero_extend 8) T1_10533) (_ bv8 16)) ((_ zero_extend 8) T1_10532))) (= T2_10604 (bvor (bvshl ((_ zero_extend 8) T1_10605) (_ bv8 16)) ((_ zero_extend 8) T1_10604))) (= T2_10606 (bvor (bvshl ((_ zero_extend 8) T1_10607) (_ bv8 16)) ((_ zero_extend 8) T1_10606))) (= T2_10667 (bvor (bvshl ((_ zero_extend 8) T1_10668) (_ bv8 16)) ((_ zero_extend 8) T1_10667))) (= T2_10669 (bvor (bvshl ((_ zero_extend 8) T1_10670) (_ bv8 16)) ((_ zero_extend 8) T1_10669))) (= T2_10734 (bvor (bvshl ((_ zero_extend 8) T1_10735) (_ bv8 16)) ((_ zero_extend 8) T1_10734))) (= T2_10736 (bvor (bvshl ((_ zero_extend 8) T1_10737) (_ bv8 16)) ((_ zero_extend 8) T1_10736))) (= T4_11167 (bvor (bvshl (bvor (bvshl (bvor (bvshl ((_ zero_extend 24) T1_11170) (_ bv8 32)) ((_ zero_extend 24) T1_11169)) (_ bv8 32)) ((_ zero_extend 24) T1_11168)) (_ bv8 32)) ((_ zero_extend 24) T1_11167))) (bvslt (bvadd ?v_5 (bvsub (bvadd (bvadd (bvadd ?v_5 (_ bv64 32)) ?v_39) ((_ zero_extend 16) T2_10736)) ?v_5)) (_ bv0 32)) (bvult (_ bv0 32) ?v_6) (bvule (_ bv0 32) ?v_6) (bvult (_ bv0 32) ?v_7) (bvule (_ bv0 32) ?v_7) (bvult (_ bv0 32) ?v_8) (bvule (_ bv0 32) ?v_8) (bvult (_ bv0 32) ?v_9) (bvule (_ bv0 32) ?v_9) (bvult (_ bv0 32) ?v_11) (bvule (_ bv0 32) ?v_11) (= ?v_12 (_ bv0 32)) (bvult (_ bv0 32) ?v_13) (bvule (_ bv0 32) ?v_13) (not (= ?v_14 (_ bv4294967295 32))) (bvule (_ bv0 32) T4_11167) (not (= T4_11167 (_ bv11151 32))) (bvule T4_11167 (_ bv11151 32)) (not (= T4_11167 (_ bv4294967295 32))) (bvult (_ bv0 32) ?v_15) (bvule (_ bv0 32) ?v_15) (bvult (_ bv0 32) ?v_17) (bvule (_ bv0 32) ?v_17) (= ?v_18 (_ bv0 32)) (not (= ?v_0 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_0) (bvult (_ bv0 32) ?v_19) (bvule (_ bv0 32) ?v_19) (not (= ?v_20 (_ bv4294967295 32))) (not (= ?v_10 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_10) (bvult (_ bv0 32) ?v_21) (bvule (_ bv0 32) ?v_21) (bvult (_ bv0 32) ?v_23) (bvule (_ bv0 32) ?v_23) (= ?v_24 (_ bv0 32)) (not (= ?v_1 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_1) (bvult (_ bv0 32) ?v_25) (bvule (_ bv0 32) ?v_25) (not (= ?v_26 (_ bv4294967295 32))) (not (= ?v_16 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_16) (bvult (_ bv0 32) ?v_27) (bvule (_ bv0 32) ?v_27) (bvult (_ bv0 32) ?v_29) (bvule (_ bv0 32) ?v_29) (= ?v_30 (_ bv0 32)) (not (= ?v_2 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_2) (bvult (_ bv0 32) ?v_31) (bvule (_ bv0 32) ?v_31) (not (= ?v_32 (_ bv4294967295 32))) (not (= ?v_22 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_22) (bvult (_ bv0 32) ?v_33) (bvule (_ bv0 32) ?v_33) (bvult (_ bv0 32) ?v_35) (bvule (_ bv0 32) ?v_35) (= ?v_36 (_ bv0 32)) (not (= ?v_3 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_3) (bvult (_ bv0 32) ?v_37) (bvule (_ bv0 32) ?v_37) (not (= ?v_38 (_ bv4294967295 32))) (not (= ?v_28 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_28) (= ?v_39 (_ bv0 32)) (not (= ?v_4 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_4) (not (= ?v_40 (_ bv4294967295 32))) (not (= ?v_34 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_34) (not (= ?v_5 (_ bv4294967295 32))) (bvule (_ bv0 32) ?v_5)))))))))))))))))) +(check-sat) +(get-info :reason-unknown) +(check-sat) +(get-info :reason-unknown) +(check-sat) +(get-info :reason-unknown) +(exit) diff --git a/tests/quantifiers/testfile-trigger002.cdcl.expected b/tests/dolmen/bitv/bv2nat_bvneg.dolmen.expected similarity index 100% rename from tests/quantifiers/testfile-trigger002.cdcl.expected rename to tests/dolmen/bitv/bv2nat_bvneg.dolmen.expected diff --git a/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 b/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 new file mode 100644 index 000000000..86632001a --- /dev/null +++ b/tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) + +; This is true, but we are not able to prove it for now due to lack of +; algebraic reasoning on bit-vectors +(declare-const x (_ BitVec 64)) +(assert (distinct (bv2nat (bvneg x)) (mod (+ (bv2nat (bvnot x)) 1) 18446744073709551616))) +(check-sat) diff --git a/tests/dolmen/bitv/bv2nat_bvnot.dolmen.expected b/tests/dolmen/bitv/bv2nat_bvnot.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/dolmen/bitv/bv2nat_bvnot.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2 b/tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2 new file mode 100644 index 000000000..1a9c2446e --- /dev/null +++ b/tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) + +(declare-const x (_ BitVec 64)) +(assert (distinct (bv2nat (bvnot x)) (- 18446744073709551615 (bv2nat x)))) +(check-sat) diff --git a/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.expected b/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.smt2 b/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.smt2 new file mode 100644 index 000000000..a0c69ebf0 --- /dev/null +++ b/tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) + +(declare-const x (_ BitVec 64)) +(assert (not (and (<= (bv2nat (bvnot x)) 18446744073709551615) (<= 0 (bv2nat (bvnot x)))))) +(check-sat) diff --git a/tests/dolmen/bitv/coherence.dolmen.expected b/tests/dolmen/bitv/coherence.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/dolmen/bitv/coherence.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/dolmen/bitv/coherence.dolmen.smt2 b/tests/dolmen/bitv/coherence.dolmen.smt2 new file mode 100644 index 000000000..56027c0eb --- /dev/null +++ b/tests/dolmen/bitv/coherence.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(declare-const x (_ BitVec 2)) +(assert (= x (concat ((_ extract 0 0) x) ((_ extract 1 1) x)))) +(declare-fun f ((_ BitVec 2)) Int) +(assert (distinct (f x) (f (concat ((_ extract 0 0) x) ((_ extract 1 1) x))))) +(check-sat) diff --git a/tests/dolmen/bitv/cyclic.dolmen.expected b/tests/dolmen/bitv/cyclic.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/dolmen/bitv/cyclic.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/dolmen/bitv/cyclic.dolmen.smt2 b/tests/dolmen/bitv/cyclic.dolmen.smt2 new file mode 100644 index 000000000..f107bad7c --- /dev/null +++ b/tests/dolmen/bitv/cyclic.dolmen.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_BV) + +(declare-const x (_ BitVec 3)) +(assert (= ((_ extract 1 0) x) (bvnot ((_ extract 2 1) x)))) +(assert (= ((_ extract 0 0) x) #b0)) +(assert (distinct x #b010)) +(check-sat) diff --git a/tests/dolmen/bitv/not-contra.dolmen.expected b/tests/dolmen/bitv/not-contra.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/dolmen/bitv/not-contra.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/dolmen/bitv/not-contra.dolmen.smt2 b/tests/dolmen/bitv/not-contra.dolmen.smt2 new file mode 100644 index 000000000..40534c7fb --- /dev/null +++ b/tests/dolmen/bitv/not-contra.dolmen.smt2 @@ -0,0 +1,7 @@ +(set-logic BV) +(set-option :produce-models true) + +(declare-const x (_ BitVec 2)) +(assert (= (bvnot x) #b00)) +(assert (= x #b00)) +(check-sat) diff --git a/tests/dolmen/bitv/notextract.dolmen.expected b/tests/dolmen/bitv/notextract.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/dolmen/bitv/notextract.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/dolmen/bitv/notextract.dolmen.smt2 b/tests/dolmen/bitv/notextract.dolmen.smt2 new file mode 100644 index 000000000..981a3e4d3 --- /dev/null +++ b/tests/dolmen/bitv/notextract.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_BV) + +(declare-const x (_ BitVec 64)) +(declare-const y (_ BitVec 64)) + +(assert (= ((_ extract 32 16) x) (bvnot ((_ extract 32 16) y)))) +(assert (= ((_ extract 32 0) x) ((_ extract 32 0) y))) +(check-sat) diff --git a/tests/dolmen/bitv/notnotx.dolmen.expected b/tests/dolmen/bitv/notnotx.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/dolmen/bitv/notnotx.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/dolmen/bitv/notnotx.dolmen.smt2 b/tests/dolmen/bitv/notnotx.dolmen.smt2 new file mode 100644 index 000000000..a81dde5c2 --- /dev/null +++ b/tests/dolmen/bitv/notnotx.dolmen.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_BV) + +(declare-const x (_ BitVec 64)) +(assert (distinct (bvnot (bvnot x)) x)) +(check-sat) diff --git a/tests/dolmen/bitv/notx.dolmen.expected b/tests/dolmen/bitv/notx.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/dolmen/bitv/notx.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/dolmen/bitv/notx.dolmen.smt2 b/tests/dolmen/bitv/notx.dolmen.smt2 new file mode 100644 index 000000000..ab8f9f6c6 --- /dev/null +++ b/tests/dolmen/bitv/notx.dolmen.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_BV) + +(declare-const x (_ BitVec 64)) +(assert (= (bvnot x) x)) +(check-sat) diff --git a/tests/float/test_float1.dolmen.expected b/tests/float/test_float1.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/float/test_float1.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/float/test_float1.dolmen.smt2 b/tests/float/test_float1.dolmen.smt2 new file mode 100644 index 000000000..94eb55117 --- /dev/null +++ b/tests/float/test_float1.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) + +(declare-const x Real) +(assert (> x 0.0)) +(assert (= ((_ ae.round 1 1) RTZ 0.3) x)) +(check-sat) \ No newline at end of file diff --git a/tests/float/test_float2.models.expected b/tests/float/test_float2.models.expected new file mode 100644 index 000000000..e9e394a51 --- /dev/null +++ b/tests/float/test_float2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () Real (/ 1 4)) +) diff --git a/tests/float/test_float2.models.smt2 b/tests/float/test_float2.models.smt2 new file mode 100644 index 000000000..1a51c4e27 --- /dev/null +++ b/tests/float/test_float2.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) + +(set-option :produce-models true) +(declare-const x Real) +(assert (> x 0.0)) +(assert (= ((_ ae.round 1 2) RTZ 0.3) x)) +(check-sat) +(get-model) \ No newline at end of file diff --git a/tests/issues/1163.cdcl.expected b/tests/issues/1163.models.expected similarity index 100% rename from tests/issues/1163.cdcl.expected rename to tests/issues/1163.models.expected diff --git a/tests/issues/1163.cdcl.smt2 b/tests/issues/1163.models.smt2 similarity index 100% rename from tests/issues/1163.cdcl.smt2 rename to tests/issues/1163.models.smt2 diff --git a/tests/issues/555.models.expected b/tests/issues/555.models.expected new file mode 100644 index 000000000..f5b97ee0b --- /dev/null +++ b/tests/issues/555.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun x () Int 0) + (define-fun y () Int 0) + (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) +) diff --git a/tests/issues/555.models.smt2 b/tests/issues/555.models.smt2 new file mode 100644 index 000000000..6c9d2634f --- /dev/null +++ b/tests/issues/555.models.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x Int) +(declare-const y Int) +(declare-const a1 (Array Int Int)) +(declare-const a2 (Array Int Int)) +(assert (= (select a1 x) x)) +(assert (= (store a1 x y) a1)) +(assert (= (select a2 x) x)) +(assert (= (store a2 x y) a1)) +(check-sat) +(get-model) diff --git a/tests/smtlib/testfile-push-pop2.cdcl.expected b/tests/issues/649/649.dolmen.expected similarity index 100% rename from tests/smtlib/testfile-push-pop2.cdcl.expected rename to tests/issues/649/649.dolmen.expected diff --git a/tests/issues/649/649.dolmen.smt2 b/tests/issues/649/649.dolmen.smt2 new file mode 100644 index 000000000..588a1f995 --- /dev/null +++ b/tests/issues/649/649.dolmen.smt2 @@ -0,0 +1,10 @@ +(set-logic BV) +(declare-const x (_ BitVec 2)) +(assert ( + exists + ((y (_ BitVec 4))) + (distinct + (concat (concat ((_ extract 3 3) y) ((_ extract 3 3) y)) y) + (concat (concat (_ bv0 2) x) (_ bv0 2)) +))) +(check-sat) diff --git a/tests/issues/664/664.dolmen.expected b/tests/issues/664/664.dolmen.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/664/664.dolmen.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/issues/664/664.dolmen.smt2 b/tests/issues/664/664.dolmen.smt2 new file mode 100644 index 000000000..e329197eb --- /dev/null +++ b/tests/issues/664/664.dolmen.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_BV) +(declare-fun T () (_ BitVec 2)) +(assert + (and + (distinct T (_ bv0 2)) + (= (_ bv0 2) (concat (_ bv0 1) ((_ extract 0 0) T))))) +(check-sat) diff --git a/tests/issues/777.models.expected b/tests/issues/777.models.expected new file mode 100644 index 000000000..8d04d7d4b --- /dev/null +++ b/tests/issues/777.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun i () Int 1) +) diff --git a/tests/issues/777.models.smt2 b/tests/issues/777.models.smt2 new file mode 100644 index 000000000..7116c6ba2 --- /dev/null +++ b/tests/issues/777.models.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const i Int) +(define-fun C ((j Int)) Bool (> j 0)) +(assert (C i)) +(check-sat) +(get-model) diff --git a/tests/issues/854/function.models.expected b/tests/issues/854/function.models.expected new file mode 100644 index 000000000..63577badc --- /dev/null +++ b/tests/issues/854/function.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun a () Int 0) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun f ((_arg_0 Int)) Int 0) + (define-fun a1 () Int 0) +) diff --git a/tests/issues/854/function.models.smt2 b/tests/issues/854/function.models.smt2 new file mode 100644 index 000000000..57ef18bcd --- /dev/null +++ b/tests/issues/854/function.models.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :smt-lib-version 2.6) +(set-option :produce-models true) +(declare-sort intref 0) +(declare-fun intrefqtmk (Int) intref) +(declare-fun a () Int) +(declare-fun f (Int) Int) +(define-fun aqtunused ((_x Int)) intref (intrefqtmk (f a))) +(assert (= (aqtunused 0) (aqtunused 1))) +(declare-fun a1 () Int) +(assert (not (and (<= 5 a1) (<= a1 15)))) +(check-sat) +(get-model) diff --git a/tests/issues/854/original.models.expected b/tests/issues/854/original.models.expected new file mode 100644 index 000000000..a0ce9f571 --- /dev/null +++ b/tests/issues/854/original.models.expected @@ -0,0 +1,7 @@ + +unknown +( + (define-fun a () Int 0) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a3 intref)) + (define-fun a1 () Int 0) +) diff --git a/tests/issues/854/original.models.smt2 b/tests/issues/854/original.models.smt2 new file mode 100644 index 000000000..fd66489a1 --- /dev/null +++ b/tests/issues/854/original.models.smt2 @@ -0,0 +1,11 @@ +(set-logic ALL) +(set-info :smt-lib-version 2.6) +(set-option :produce-models true) +(declare-sort intref 0) +(declare-fun intrefqtmk (Int) intref) +(declare-fun a () Int) +(define-fun aqtunused () intref (intrefqtmk a)) +(declare-fun a1 () Int) +(assert (not (and (<= 5 a1) (<= a1 15)))) +(check-sat) +(get-model) diff --git a/tests/issues/854/twice_eq.models.expected b/tests/issues/854/twice_eq.models.expected new file mode 100644 index 000000000..3488c940f --- /dev/null +++ b/tests/issues/854/twice_eq.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun a () Int 0) + (define-fun intrefqtmk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun another_mk ((_arg_0 Int)) intref (as @a4 intref)) + (define-fun a1 () Int 0) +) diff --git a/tests/issues/854/twice_eq.models.smt2 b/tests/issues/854/twice_eq.models.smt2 new file mode 100644 index 000000000..eaac2b8d6 --- /dev/null +++ b/tests/issues/854/twice_eq.models.smt2 @@ -0,0 +1,13 @@ +(set-logic ALL) +(set-info :smt-lib-version 2.6) +(set-option :produce-models true) +(declare-sort intref 0) +(declare-fun intrefqtmk (Int) intref) +(declare-fun another_mk (Int) intref) +(declare-fun a () Int) +(define-fun aqtunused () intref (intrefqtmk a)) +(assert (= aqtunused (another_mk a))) +(declare-fun a1 () Int) +(assert (not (and (<= 5 a1) (<= a1 15)))) +(check-sat) +(get-model) diff --git a/tests/issues/883.dolmen.expected b/tests/issues/883.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/issues/883.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/issues/883.dolmen.smt2 b/tests/issues/883.dolmen.smt2 new file mode 100644 index 000000000..75a70f619 --- /dev/null +++ b/tests/issues/883.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(declare-const x Int) +(assert (= ((_ int2bv 2) x) #b11)) +(assert (<= x 0)) +(assert (<= 0 x)) +(check-sat) diff --git a/tests/issues/926.models.expected b/tests/issues/926.models.expected new file mode 100644 index 000000000..4c3eea7da --- /dev/null +++ b/tests/issues/926.models.expected @@ -0,0 +1,10 @@ + +unknown +( + (define-fun x1 () Int 5) + (define-fun x2 () Int (- 5)) + (define-fun y1 () Real (/ 3 2)) + (define-fun y2 () Real 4.0) + (define-fun y3 () Real (/ 16 5)) + (define-fun y4 () Real (/ (- 3) 2)) +) diff --git a/tests/issues/926.models.smt2 b/tests/issues/926.models.smt2 new file mode 100644 index 000000000..2c9860dae --- /dev/null +++ b/tests/issues/926.models.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x1 Int) +(declare-const x2 Int) +(declare-const y1 Real) +(declare-const y2 Real) +(declare-const y3 Real) +(declare-const y4 Real) +(assert (= x1 5)) +(assert (= x2 (- 5))) +(assert (= y1 (/ (- 3.0) (- 2.0)))) +(assert (= y2 (/ (- 4.0) (- 1.0)))) +(assert (= y3 3.2)) +(assert (= y4 (/ 3.0 (- 2.0)))) +(check-sat) +(get-model) diff --git a/tests/issues/1024.err.cdcl.expected b/tests/issues/issue1024.err.dolmen.expected similarity index 100% rename from tests/issues/1024.err.cdcl.expected rename to tests/issues/issue1024.err.dolmen.expected diff --git a/tests/issues/1024.err.cdcl.smt2 b/tests/issues/issue1024.err.dolmen.smt2 similarity index 100% rename from tests/issues/1024.err.cdcl.smt2 rename to tests/issues/issue1024.err.dolmen.smt2 diff --git a/tests/models/adt/arith.models.expected b/tests/models/adt/arith.models.expected new file mode 100644 index 000000000..18e539f31 --- /dev/null +++ b/tests/models/adt/arith.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun x () Real 2.0) + (define-fun y () Real 0.0) + (define-fun a () Data (cons1 2.0 0.0)) + (define-fun b () Data (cons3 0.0)) +) diff --git a/tests/models/adt/arith.models.smt2 b/tests/models/adt/arith.models.smt2 new file mode 100644 index 000000000..e1bb69775 --- /dev/null +++ b/tests/models/adt/arith.models.smt2 @@ -0,0 +1,18 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatype Data ( + (cons1 (d1 Real) (d2 Real)) + (cons2) + (cons3 (d3 Real)) +)) +(declare-const a Data) +(declare-const b Data) +(declare-const x Real) +(declare-const y Real) +(assert ((_ is cons1) a)) +(assert ((_ is cons3) b)) +(assert (= (d1 a) x)) +(assert (= (d3 b) y)) +(assert (= (d1 a) (- 2 (d3 b)))) +(check-sat) +(get-model) diff --git a/tests/models/adt/list.models.expected b/tests/models/adt/list.models.expected new file mode 100644 index 000000000..07eb25ebb --- /dev/null +++ b/tests/models/adt/list.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun a () List empty) + (define-fun b () List empty) + (define-fun c () List (cons 0 empty)) + (define-fun d () List empty) +) diff --git a/tests/models/adt/list.models.smt2 b/tests/models/adt/list.models.smt2 new file mode 100644 index 000000000..33dda60cc --- /dev/null +++ b/tests/models/adt/list.models.smt2 @@ -0,0 +1,15 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatype List ( + (empty) + (cons (head Int) (tail List)) +)) +(declare-const a List) +(declare-const b List) +(declare-const c List) +(declare-const d List) +(assert (= (tail a) b)) +(assert ((_ is cons) c)) +(assert (= (tail c) d)) +(check-sat) +(get-model) diff --git a/tests/models/adt/rec.models.expected b/tests/models/adt/rec.models.expected new file mode 100644 index 000000000..3cac54112 --- /dev/null +++ b/tests/models/adt/rec.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () data (cons1 cons2)) +) diff --git a/tests/models/adt/rec.models.smt2 b/tests/models/adt/rec.models.smt2 new file mode 100644 index 000000000..d724e94f5 --- /dev/null +++ b/tests/models/adt/rec.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatype data ( + (cons1 (d1 data)) + (cons2) +)) +(declare-const a data) +(assert ((_ is cons1) a)) +(check-sat) +(get-model) diff --git a/tests/models/adt/rec2.models.expected b/tests/models/adt/rec2.models.expected new file mode 100644 index 000000000..d5a224aa4 --- /dev/null +++ b/tests/models/adt/rec2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () data1 (cons1 (cons2 cons4))) +) diff --git a/tests/models/adt/rec2.models.smt2 b/tests/models/adt/rec2.models.smt2 new file mode 100644 index 000000000..511d9a5a8 --- /dev/null +++ b/tests/models/adt/rec2.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes ((data1 0) (data2 0)) ( + ((cons1 (d1 data1)) (cons2 (d2 data2))) + ((cons3 (d3 data1)) (cons4)) +)) +(declare-const a data1) +(assert ((_ is cons1) a)) +(check-sat) +(get-model) diff --git a/tests/models/adt/rec3.models.expected b/tests/models/adt/rec3.models.expected new file mode 100644 index 000000000..271412502 --- /dev/null +++ b/tests/models/adt/rec3.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () data1 (cons1 (cons2 (cons4 0 1)))) +) diff --git a/tests/models/adt/rec3.models.smt2 b/tests/models/adt/rec3.models.smt2 new file mode 100644 index 000000000..6b23dc3f0 --- /dev/null +++ b/tests/models/adt/rec3.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes ((data1 0) (data2 0)) ( + ((cons1 (d1 data1)) (cons2 (d2 data2))) + ((cons3 (d3 data1)) (cons4 (d4 Int) (d5 Int))) +)) +(declare-const a data1) +(assert ((_ is cons1) a)) +(check-sat) +(get-model) diff --git a/tests/models/adt/small.models.expected b/tests/models/adt/small.models.expected new file mode 100644 index 000000000..a0f6a5ba5 --- /dev/null +++ b/tests/models/adt/small.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () data1 (cons1 (cons2 (cons5 false)))) +) diff --git a/tests/models/adt/small.models.smt2 b/tests/models/adt/small.models.smt2 new file mode 100644 index 000000000..b03dd5902 --- /dev/null +++ b/tests/models/adt/small.models.smt2 @@ -0,0 +1,11 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes ((data1 0) (data2 0)) ( + ((cons1 (d1 data1)) (cons2 (d2 data2))) + ((cons3 (d3 data1)) (cons4 (d4 Int) (d5 Int) (d6 Bool)) + (cons5 (d7 Bool))) +)) +(declare-const a data1) +(assert ((_ is cons1) a)) +(check-sat) +(get-model) diff --git a/tests/models/arith/arith1.models.expected b/tests/models/arith/arith1.models.expected new file mode 100644 index 000000000..456e0f19d --- /dev/null +++ b/tests/models/arith/arith1.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () Int 0) +) diff --git a/tests/models/arith/arith1.models.smt2 b/tests/models/arith/arith1.models.smt2 new file mode 100644 index 000000000..b625bd962 --- /dev/null +++ b/tests/models/arith/arith1.models.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x Int) +(assert (<= x 42)) +(check-sat) +(get-model) diff --git a/tests/models/arith/arith10.cdcl.expected b/tests/models/arith/arith10.dolmen.expected similarity index 100% rename from tests/models/arith/arith10.cdcl.expected rename to tests/models/arith/arith10.dolmen.expected diff --git a/tests/models/arith/arith10.cdcl.smt2 b/tests/models/arith/arith10.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith10.cdcl.smt2 rename to tests/models/arith/arith10.dolmen.smt2 diff --git a/tests/models/arith/arith11.cdcl.expected b/tests/models/arith/arith11.dolmen.expected similarity index 100% rename from tests/models/arith/arith11.cdcl.expected rename to tests/models/arith/arith11.dolmen.expected diff --git a/tests/models/arith/arith11.cdcl.smt2 b/tests/models/arith/arith11.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith11.cdcl.smt2 rename to tests/models/arith/arith11.dolmen.smt2 diff --git a/tests/models/arith/arith12.cdcl.expected b/tests/models/arith/arith12.dolmen.expected similarity index 100% rename from tests/models/arith/arith12.cdcl.expected rename to tests/models/arith/arith12.dolmen.expected diff --git a/tests/models/arith/arith12.cdcl.smt2 b/tests/models/arith/arith12.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith12.cdcl.smt2 rename to tests/models/arith/arith12.dolmen.smt2 diff --git a/tests/models/arith/arith13.cdcl.expected b/tests/models/arith/arith13.models.expected similarity index 100% rename from tests/models/arith/arith13.cdcl.expected rename to tests/models/arith/arith13.models.expected diff --git a/tests/models/arith/arith13.cdcl.smt2 b/tests/models/arith/arith13.models.smt2 similarity index 100% rename from tests/models/arith/arith13.cdcl.smt2 rename to tests/models/arith/arith13.models.smt2 diff --git a/tests/models/arith/arith14.cdcl.expected b/tests/models/arith/arith14.models.expected similarity index 100% rename from tests/models/arith/arith14.cdcl.expected rename to tests/models/arith/arith14.models.expected diff --git a/tests/models/arith/arith14.cdcl.smt2 b/tests/models/arith/arith14.models.smt2 similarity index 100% rename from tests/models/arith/arith14.cdcl.smt2 rename to tests/models/arith/arith14.models.smt2 diff --git a/tests/models/arith/arith15.cdcl.expected b/tests/models/arith/arith15.models.expected similarity index 100% rename from tests/models/arith/arith15.cdcl.expected rename to tests/models/arith/arith15.models.expected diff --git a/tests/models/arith/arith15.cdcl.smt2 b/tests/models/arith/arith15.models.smt2 similarity index 100% rename from tests/models/arith/arith15.cdcl.smt2 rename to tests/models/arith/arith15.models.smt2 diff --git a/tests/models/arith/arith2.models.expected b/tests/models/arith/arith2.models.expected new file mode 100644 index 000000000..65e06f1f6 --- /dev/null +++ b/tests/models/arith/arith2.models.expected @@ -0,0 +1,6 @@ + +unknown +( + (define-fun x () Int 8) + (define-fun y () Int 42) +) diff --git a/tests/models/arith/arith2.models.smt2 b/tests/models/arith/arith2.models.smt2 new file mode 100644 index 000000000..e35b93112 --- /dev/null +++ b/tests/models/arith/arith2.models.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x Int) +(declare-const y Int) +(assert (and (<= x 42) (>= x 0) (>= y 42) (= (+ x y) 50))) +(check-sat) +(get-model) diff --git a/tests/models/arith/arith3.cdcl.expected b/tests/models/arith/arith3.dolmen.expected similarity index 100% rename from tests/models/arith/arith3.cdcl.expected rename to tests/models/arith/arith3.dolmen.expected diff --git a/tests/models/arith/arith3.cdcl.smt2 b/tests/models/arith/arith3.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith3.cdcl.smt2 rename to tests/models/arith/arith3.dolmen.smt2 diff --git a/tests/models/arith/arith4.cdcl.expected b/tests/models/arith/arith4.dolmen.expected similarity index 100% rename from tests/models/arith/arith4.cdcl.expected rename to tests/models/arith/arith4.dolmen.expected diff --git a/tests/models/arith/arith4.cdcl.smt2 b/tests/models/arith/arith4.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith4.cdcl.smt2 rename to tests/models/arith/arith4.dolmen.smt2 diff --git a/tests/models/arith/arith5.cdcl.expected b/tests/models/arith/arith5.dolmen.expected similarity index 100% rename from tests/models/arith/arith5.cdcl.expected rename to tests/models/arith/arith5.dolmen.expected diff --git a/tests/models/arith/arith5.cdcl.smt2 b/tests/models/arith/arith5.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith5.cdcl.smt2 rename to tests/models/arith/arith5.dolmen.smt2 diff --git a/tests/models/arith/arith6.cdcl.expected b/tests/models/arith/arith6.dolmen.expected similarity index 100% rename from tests/models/arith/arith6.cdcl.expected rename to tests/models/arith/arith6.dolmen.expected diff --git a/tests/models/arith/arith6.cdcl.smt2 b/tests/models/arith/arith6.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith6.cdcl.smt2 rename to tests/models/arith/arith6.dolmen.smt2 diff --git a/tests/models/arith/arith7.cdcl.expected b/tests/models/arith/arith7.dolmen.expected similarity index 100% rename from tests/models/arith/arith7.cdcl.expected rename to tests/models/arith/arith7.dolmen.expected diff --git a/tests/models/arith/arith7.cdcl.smt2 b/tests/models/arith/arith7.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith7.cdcl.smt2 rename to tests/models/arith/arith7.dolmen.smt2 diff --git a/tests/models/arith/arith8.cdcl.expected b/tests/models/arith/arith8.dolmen.expected similarity index 100% rename from tests/models/arith/arith8.cdcl.expected rename to tests/models/arith/arith8.dolmen.expected diff --git a/tests/models/arith/arith8.cdcl.smt2 b/tests/models/arith/arith8.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith8.cdcl.smt2 rename to tests/models/arith/arith8.dolmen.smt2 diff --git a/tests/models/arith/arith9.cdcl.expected b/tests/models/arith/arith9.dolmen.expected similarity index 100% rename from tests/models/arith/arith9.cdcl.expected rename to tests/models/arith/arith9.dolmen.expected diff --git a/tests/models/arith/arith9.cdcl.smt2 b/tests/models/arith/arith9.dolmen.smt2 similarity index 100% rename from tests/models/arith/arith9.cdcl.smt2 rename to tests/models/arith/arith9.dolmen.smt2 diff --git a/tests/models/array/array1.models.expected b/tests/models/array/array1.models.expected new file mode 100644 index 000000000..f5b97ee0b --- /dev/null +++ b/tests/models/array/array1.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun x () Int 0) + (define-fun y () Int 0) + (define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0)) + (define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0)) +) diff --git a/tests/models/array/array1.models.smt2 b/tests/models/array/array1.models.smt2 new file mode 100644 index 000000000..6c9d2634f --- /dev/null +++ b/tests/models/array/array1.models.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x Int) +(declare-const y Int) +(declare-const a1 (Array Int Int)) +(declare-const a2 (Array Int Int)) +(assert (= (select a1 x) x)) +(assert (= (store a1 x y) a1)) +(assert (= (select a2 x) x)) +(assert (= (store a2 x y) a1)) +(check-sat) +(get-model) diff --git a/tests/models/array/embedded-array.models.expected b/tests/models/array/embedded-array.models.expected new file mode 100644 index 000000000..0cb5c3d3e --- /dev/null +++ b/tests/models/array/embedded-array.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun x () Pair + (pair (store (as @a3 (Array Int S)) 0 s) + (store (as @a3 (Array Int S)) 0 s))) + (define-fun s () S (as @a2 S)) +) diff --git a/tests/models/array/embedded-array.models.smt2 b/tests/models/array/embedded-array.models.smt2 new file mode 100644 index 000000000..fa76cb828 --- /dev/null +++ b/tests/models/array/embedded-array.models.smt2 @@ -0,0 +1,10 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-sort S 0) +(declare-const s S) +(declare-datatype Pair ((pair (first (Array Int S)) (second (Array Int S))))) +(declare-const x Pair) +(assert (= (select (first x) 0) s)) +(assert (= (first x) (second x))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/bvand-1.models.expected b/tests/models/bitv/bvand-1.models.expected new file mode 100644 index 000000000..97dc85664 --- /dev/null +++ b/tests/models/bitv/bvand-1.models.expected @@ -0,0 +1,6 @@ + +unknown +( + (define-fun x () (_ BitVec 8) #xa5) + (define-fun y () (_ BitVec 8) #x5a) +) diff --git a/tests/models/bitv/bvand-1.models.smt2 b/tests/models/bitv/bvand-1.models.smt2 new file mode 100644 index 000000000..01b3171f9 --- /dev/null +++ b/tests/models/bitv/bvand-1.models.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x (_ BitVec 8)) +(declare-const y (_ BitVec 8)) +; This forces the values of x and y and (= x (bvnot y)) +(assert (= x (bvand #b10100101 (bvnot y)))) +(assert (= y (bvand #b01011010 (bvnot x)))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/bvand-2.models.expected b/tests/models/bitv/bvand-2.models.expected new file mode 100644 index 000000000..389856c52 --- /dev/null +++ b/tests/models/bitv/bvand-2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () (_ BitVec 8) #x05) +) diff --git a/tests/models/bitv/bvand-2.models.smt2 b/tests/models/bitv/bvand-2.models.smt2 new file mode 100644 index 000000000..d9533feaf --- /dev/null +++ b/tests/models/bitv/bvand-2.models.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x (_ BitVec 8)) +(assert (= x (bvand #b10100101 #b01010101))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/bvor-1.models.expected b/tests/models/bitv/bvor-1.models.expected new file mode 100644 index 000000000..a9cd47cf5 --- /dev/null +++ b/tests/models/bitv/bvor-1.models.expected @@ -0,0 +1,6 @@ + +unknown +( + (define-fun x () (_ BitVec 8) #xff) + (define-fun y () (_ BitVec 8) #xff) +) diff --git a/tests/models/bitv/bvor-1.models.smt2 b/tests/models/bitv/bvor-1.models.smt2 new file mode 100644 index 000000000..15887d902 --- /dev/null +++ b/tests/models/bitv/bvor-1.models.smt2 @@ -0,0 +1,9 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x (_ BitVec 8)) +(declare-const y (_ BitVec 8)) +; This forces the values of x and y to all ones +(assert (= x (bvor #b10100101 y))) +(assert (= y (bvor #b01011010 x))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/bvor-2.models.expected b/tests/models/bitv/bvor-2.models.expected new file mode 100644 index 000000000..3d9364421 --- /dev/null +++ b/tests/models/bitv/bvor-2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () (_ BitVec 8) #xf5) +) diff --git a/tests/models/bitv/bvor-2.models.smt2 b/tests/models/bitv/bvor-2.models.smt2 new file mode 100644 index 000000000..7a11b51b5 --- /dev/null +++ b/tests/models/bitv/bvor-2.models.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x (_ BitVec 8)) +(assert (= x (bvor #b10100101 #b01010101))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/bvxor-1.models.expected b/tests/models/bitv/bvxor-1.models.expected new file mode 100644 index 000000000..a131f5562 --- /dev/null +++ b/tests/models/bitv/bvxor-1.models.expected @@ -0,0 +1,6 @@ + +unknown +( + (define-fun x () (_ BitVec 8) #x00) + (define-fun y () (_ BitVec 8) #xa5) +) diff --git a/tests/models/bitv/bvxor-1.models.smt2 b/tests/models/bitv/bvxor-1.models.smt2 new file mode 100644 index 000000000..75e678c93 --- /dev/null +++ b/tests/models/bitv/bvxor-1.models.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x (_ BitVec 8)) +(declare-const y (_ BitVec 8)) +(assert (= x (bvxor #b10100101 y))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/bvxor-2.models.expected b/tests/models/bitv/bvxor-2.models.expected new file mode 100644 index 000000000..2519dac8a --- /dev/null +++ b/tests/models/bitv/bvxor-2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () (_ BitVec 8) #xf0) +) diff --git a/tests/models/bitv/bvxor-2.models.smt2 b/tests/models/bitv/bvxor-2.models.smt2 new file mode 100644 index 000000000..dc497a356 --- /dev/null +++ b/tests/models/bitv/bvxor-2.models.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x (_ BitVec 8)) +(assert (= x (bvxor #b10100101 #b01010101))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/cardinal.models.expected b/tests/models/bitv/cardinal.models.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/models/bitv/cardinal.models.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/models/bitv/cardinal.models.smt2 b/tests/models/bitv/cardinal.models.smt2 new file mode 100644 index 000000000..04c0ab2f1 --- /dev/null +++ b/tests/models/bitv/cardinal.models.smt2 @@ -0,0 +1,11 @@ +(set-logic BV) +(set-option :produce-models true) + +; We used to be able to reply 'unsat' here, but using unsound reasoning. +; We should be able to reply 'unsat' again when we start propagating [distinct] +; constraints in the bit-vector domain +(declare-const a (_ BitVec 1)) +(declare-const b (_ BitVec 1)) +(declare-const c (_ BitVec 1)) +(assert (distinct a b c)) +(check-sat) diff --git a/tests/models/bitv/cs-soundness.models.expected b/tests/models/bitv/cs-soundness.models.expected new file mode 100644 index 000000000..4950a8256 --- /dev/null +++ b/tests/models/bitv/cs-soundness.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () (_ BitVec 2) #b01) +) diff --git a/tests/models/bitv/cs-soundness.models.smt2 b/tests/models/bitv/cs-soundness.models.smt2 new file mode 100644 index 000000000..78d78ade5 --- /dev/null +++ b/tests/models/bitv/cs-soundness.models.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_BV) +(set-option :produce-models true) +(set-info :status sat) +(declare-fun a () (_ BitVec 2)) +(assert (not (bvslt a #b01))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/extract.models.expected b/tests/models/bitv/extract.models.expected new file mode 100644 index 000000000..16b1f5e3a --- /dev/null +++ b/tests/models/bitv/extract.models.expected @@ -0,0 +1,8 @@ + +unknown +( + (define-fun a () (_ BitVec 2) #b11) + (define-fun b () (_ BitVec 3) #b111) + (define-fun c () (_ BitVec 6) #b111011) + (define-fun z () (_ BitVec 1) #b0) +) diff --git a/tests/models/bitv/extract.models.smt2 b/tests/models/bitv/extract.models.smt2 new file mode 100644 index 000000000..0233d238a --- /dev/null +++ b/tests/models/bitv/extract.models.smt2 @@ -0,0 +1,18 @@ +(set-logic BV) +(set-option :produce-models true) + +(declare-const a (_ BitVec 2)) +(declare-const b (_ BitVec 3)) +(declare-const c (_ BitVec 6)) +(declare-const z (_ BitVec 1)) + +(assert (= ((_ extract 0 0) c) #b1)) +(assert (= ((_ extract 5 5) c) #b1)) +(assert (= (concat (concat b z) a) c)) + +(assert (= ((_ extract 1 1) a) #b1)) +(assert (= ((_ extract 1 0) b) #b11)) +(assert (= z #b0)) + +(check-sat) +(get-model) diff --git a/tests/models/bitv/manyslice.models.expected b/tests/models/bitv/manyslice.models.expected new file mode 100644 index 000000000..5faea754b --- /dev/null +++ b/tests/models/bitv/manyslice.models.expected @@ -0,0 +1,7 @@ + +unknown +( + (define-fun x () (_ BitVec 1) #b1) + (define-fun y () (_ BitVec 1) #b0) + (define-fun xy () (_ BitVec 2) #b10) +) diff --git a/tests/models/bitv/manyslice.models.smt2 b/tests/models/bitv/manyslice.models.smt2 new file mode 100644 index 000000000..a7813ed5d --- /dev/null +++ b/tests/models/bitv/manyslice.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x (_ BitVec 1)) +(declare-const y (_ BitVec 1)) +(declare-const xy (_ BitVec 2)) +(assert (= (concat (concat x y) (concat xy xy)) (concat #b1010 (concat x y)))) +(check-sat) +(get-model) diff --git a/tests/models/bitv/not.models.expected b/tests/models/bitv/not.models.expected new file mode 100644 index 000000000..a785c1aa5 --- /dev/null +++ b/tests/models/bitv/not.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () (_ BitVec 2) #b11) +) diff --git a/tests/models/bitv/not.models.smt2 b/tests/models/bitv/not.models.smt2 new file mode 100644 index 000000000..02a77470e --- /dev/null +++ b/tests/models/bitv/not.models.smt2 @@ -0,0 +1,7 @@ +(set-logic BV) +(set-option :produce-models true) + +(declare-const x (_ BitVec 2)) +(assert (= (bvnot x) #b00)) +(check-sat) +(get-model) diff --git a/tests/models/bitv/optim-1.cdcl.expected b/tests/models/bitv/optim-1.models.expected similarity index 100% rename from tests/models/bitv/optim-1.cdcl.expected rename to tests/models/bitv/optim-1.models.expected diff --git a/tests/models/bitv/optim-1.cdcl.smt2 b/tests/models/bitv/optim-1.models.smt2 similarity index 100% rename from tests/models/bitv/optim-1.cdcl.smt2 rename to tests/models/bitv/optim-1.models.smt2 diff --git a/tests/models/bitv/optim-2.cdcl.expected b/tests/models/bitv/optim-2.models.expected similarity index 100% rename from tests/models/bitv/optim-2.cdcl.expected rename to tests/models/bitv/optim-2.models.expected diff --git a/tests/models/bitv/optim-2.cdcl.smt2 b/tests/models/bitv/optim-2.models.smt2 similarity index 100% rename from tests/models/bitv/optim-2.cdcl.smt2 rename to tests/models/bitv/optim-2.models.smt2 diff --git a/tests/models/bitv/optim-3.cdcl.expected b/tests/models/bitv/optim-3.models.expected similarity index 100% rename from tests/models/bitv/optim-3.cdcl.expected rename to tests/models/bitv/optim-3.models.expected diff --git a/tests/models/bitv/optim-3.cdcl.smt2 b/tests/models/bitv/optim-3.models.smt2 similarity index 100% rename from tests/models/bitv/optim-3.cdcl.smt2 rename to tests/models/bitv/optim-3.models.smt2 diff --git a/tests/models/bitv/optim-4.cdcl.expected b/tests/models/bitv/optim-4.models.expected similarity index 100% rename from tests/models/bitv/optim-4.cdcl.expected rename to tests/models/bitv/optim-4.models.expected diff --git a/tests/models/bitv/optim-4.cdcl.smt2 b/tests/models/bitv/optim-4.models.smt2 similarity index 100% rename from tests/models/bitv/optim-4.cdcl.smt2 rename to tests/models/bitv/optim-4.models.smt2 diff --git a/tests/models/bitv/optim-5.cdcl.expected b/tests/models/bitv/optim-5.models.expected similarity index 100% rename from tests/models/bitv/optim-5.cdcl.expected rename to tests/models/bitv/optim-5.models.expected diff --git a/tests/models/bitv/optim-5.cdcl.smt2 b/tests/models/bitv/optim-5.models.smt2 similarity index 100% rename from tests/models/bitv/optim-5.cdcl.smt2 rename to tests/models/bitv/optim-5.models.smt2 diff --git a/tests/models/bitv/specified.models.expected b/tests/models/bitv/specified.models.expected new file mode 100644 index 000000000..58c561fdb --- /dev/null +++ b/tests/models/bitv/specified.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () (_ BitVec 4) #x5) +) diff --git a/tests/models/bitv/specified.models.smt2 b/tests/models/bitv/specified.models.smt2 new file mode 100644 index 000000000..ade3d104f --- /dev/null +++ b/tests/models/bitv/specified.models.smt2 @@ -0,0 +1,10 @@ +(set-logic BV) +(set-option :produce-models true) + +(declare-const x (_ BitVec 4)) +(assert (= ((_ extract 0 0) x) #b1)) +(assert (= ((_ extract 1 1) x) #b0)) +(assert (= ((_ extract 2 2) x) #b1)) +(assert (= ((_ extract 3 3) x) #b0)) +(check-sat) +(get-model) diff --git a/tests/models/bool/bool1.models.expected b/tests/models/bool/bool1.models.expected new file mode 100644 index 000000000..1eb3e25e7 --- /dev/null +++ b/tests/models/bool/bool1.models.expected @@ -0,0 +1,18 @@ + +unknown +( + (define-fun p () Bool true) + (define-fun q () Bool true) +) +((notp false) + (notnq false)) + + +unknown +( + (define-fun p () Bool true) + (define-fun q () Bool true) +) +((notp false) + (notnq false)) + diff --git a/tests/models/bool/bool1.models.smt2 b/tests/models/bool/bool1.models.smt2 new file mode 100644 index 000000000..a4e6549ec --- /dev/null +++ b/tests/models/bool/bool1.models.smt2 @@ -0,0 +1,16 @@ +(set-option :produce-models true) ; enable model generation +(set-option :produce-assignments true) ; enable get assignment +(set-logic QF_UF) +(declare-const p Bool) +(declare-const q Bool) +; (declare-const t Int) +(define-fun nq () Bool q) +(assert (=> (! (not p) :named notp) (! (not nq) :named notnq))) +(check-sat) +(get-model) +(get-assignment) +(assert q) +(check-sat) +(get-model) +(get-assignment) +(exit) diff --git a/tests/models/bool/bool2.cdcl.expected b/tests/models/bool/bool2.models.expected similarity index 100% rename from tests/models/bool/bool2.cdcl.expected rename to tests/models/bool/bool2.models.expected diff --git a/tests/models/bool/bool2.cdcl.smt2 b/tests/models/bool/bool2.models.smt2 similarity index 100% rename from tests/models/bool/bool2.cdcl.smt2 rename to tests/models/bool/bool2.models.smt2 diff --git a/tests/models/bool/bool3.models.expected b/tests/models/bool/bool3.models.expected new file mode 100644 index 000000000..341a2df7e --- /dev/null +++ b/tests/models/bool/bool3.models.expected @@ -0,0 +1,9 @@ + +unknown +( + (define-fun x () Bool true) + (define-fun y () Bool true) +) +((foo true) + (bar false)) + diff --git a/tests/models/bool/bool3.models.smt2 b/tests/models/bool/bool3.models.smt2 new file mode 100644 index 000000000..1d417aec4 --- /dev/null +++ b/tests/models/bool/bool3.models.smt2 @@ -0,0 +1,9 @@ +(set-option :produce-assignments true) +(set-option :produce-models true) +(set-logic ALL) +(declare-const x Bool) +(declare-const y Bool) +(assert (or (! (and x y) :named foo) (! (and (not x) (not y)) :named bar))) +(check-sat) +(get-model) +(get-assignment) \ No newline at end of file diff --git a/tests/models/check_sat.models.ae b/tests/models/check_sat.models.ae new file mode 100644 index 000000000..e73de98ae --- /dev/null +++ b/tests/models/check_sat.models.ae @@ -0,0 +1,8 @@ +logic x : int + +axiom x_gt_0 : x > 0 + +check_sat cs_x_lt_0: x < 0 +check_sat cs_x_gt_0: x > 0 +goal g_x_lt_0: x < 0 +goal g_x_gt_0: x > 0 diff --git a/tests/models/check_sat.models.expected b/tests/models/check_sat.models.expected new file mode 100644 index 000000000..60f5071ce --- /dev/null +++ b/tests/models/check_sat.models.expected @@ -0,0 +1,8 @@ + +unsat + +unknown + +unknown + +unsat diff --git a/tests/models/complete_3.cdcl.expected b/tests/models/complete_1.models.expected similarity index 100% rename from tests/models/complete_3.cdcl.expected rename to tests/models/complete_1.models.expected diff --git a/tests/models/complete_1.models.smt2 b/tests/models/complete_1.models.smt2 new file mode 100644 index 000000000..8cf1fbe1c --- /dev/null +++ b/tests/models/complete_1.models.smt2 @@ -0,0 +1,8 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-const x Int) +; The preprocessor will replace this equation by `true` but we still +; have to produce a model value for `x`. +(assert (= x x)) +(check-sat) +(get-model) diff --git a/tests/models/complete_2.models.expected b/tests/models/complete_2.models.expected new file mode 100644 index 000000000..09be59233 --- /dev/null +++ b/tests/models/complete_2.models.expected @@ -0,0 +1,6 @@ + +unknown +( + (define-fun x () Int (as @a1 Int)) + (define-fun f ((_arg_0 Int)) Int (as @a0 Int)) +) diff --git a/tests/models/complete_2.models.smt2 b/tests/models/complete_2.models.smt2 new file mode 100644 index 000000000..448e572dd --- /dev/null +++ b/tests/models/complete_2.models.smt2 @@ -0,0 +1,8 @@ +(set-option :produce-models true) +(set-logic ALL) +(declare-const x Int) +(declare-fun f (Int) Int) +; There is no constraint on `x` and `f` but we still have to produce a model +; value for them. +(check-sat) +(get-model) diff --git a/tests/models/complete_3.models.expected b/tests/models/complete_3.models.expected new file mode 100644 index 000000000..d507e21ca --- /dev/null +++ b/tests/models/complete_3.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun x () Int (as @a0 Int)) +) diff --git a/tests/models/complete_3.cdcl.smt2 b/tests/models/complete_3.models.smt2 similarity index 100% rename from tests/models/complete_3.cdcl.smt2 rename to tests/models/complete_3.models.smt2 diff --git a/tests/models/issues/715/715_1.models.ae b/tests/models/issues/715/715_1.models.ae new file mode 100644 index 000000000..84ef6c34f --- /dev/null +++ b/tests/models/issues/715/715_1.models.ae @@ -0,0 +1,6 @@ +logic f: int + +(* This function is user-defined and shouldn't appear in the output model. *) +function g(x: int, y: int) : int = x + y + +check_sat t: f = 0 diff --git a/tests/models/issues/715/715_1.models.expected b/tests/models/issues/715/715_1.models.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/models/issues/715/715_1.models.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/models/issues/715/715_2.models.expected b/tests/models/issues/715/715_2.models.expected new file mode 100644 index 000000000..966bb2f29 --- /dev/null +++ b/tests/models/issues/715/715_2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun f () Int 0) +) diff --git a/tests/models/issues/715/715_2.models.smt2 b/tests/models/issues/715/715_2.models.smt2 new file mode 100644 index 000000000..93a28138c --- /dev/null +++ b/tests/models/issues/715/715_2.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const f Int) +(assert (= f 0)) +; This function is user-defined and shouldn't appear in the output model. +(define-fun g ((x Int) (y Int)) Int (+ x y)) +(check-sat) +(get-model) diff --git a/tests/models/issues/719.models.err.expected b/tests/models/issues/719.models.err.expected new file mode 100644 index 000000000..1b1ed6e84 --- /dev/null +++ b/tests/models/issues/719.models.err.expected @@ -0,0 +1,3 @@ + +unsat +(error "No model produced.") diff --git a/tests/models/issues/719.models.err.smt2 b/tests/models/issues/719.models.err.smt2 new file mode 100644 index 000000000..66c07f37c --- /dev/null +++ b/tests/models/issues/719.models.err.smt2 @@ -0,0 +1,19 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const a (Array Int Int)) +(declare-const s Int) +(assert (and (<= 0 s) (<= s 10))) +(assert (forall ((k Int)) (=> (and (<= 0 k) (< k s)) (<= (select a k) (select a s))))) +(assert (forall ((k Int)) (=> (and (< s k) (<= k 10)) (<= (select a s) (select a k))))) +(assert ( + forall ((p Int) (q Int)) + (=> (and (<= 0 p) (< p q) (<= q (- s 1))) (<= (select a p) (select a q))))) +(assert ( + forall ((p Int) (q Int)) + (=> (and (<= (+ s 1) p) (< p q) (<= q 10)) (<= (select a p) (select a q))))) +(assert (not ( + forall ((p Int) (q Int)) + (=> (and (<= 0 p) (< p q) (<= q 10)) (<= (select a p) (select a q)))))) +(check-sat) +(get-model) +; (get-model) should fail because the problem is UNSAT. \ No newline at end of file diff --git a/tests/models/records/record1.models.expected b/tests/models/records/record1.models.expected new file mode 100644 index 000000000..da5e88f8f --- /dev/null +++ b/tests/models/records/record1.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun a () Pair (pair 5 0)) +) diff --git a/tests/models/records/record1.models.smt2 b/tests/models/records/record1.models.smt2 new file mode 100644 index 000000000..2739fc71d --- /dev/null +++ b/tests/models/records/record1.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-datatype Pair +((pair (first Int) (second Int)))) +(declare-const a Pair) +(assert (= (first a) 5)) +(check-sat) +(get-model) diff --git a/tests/models/records/record2.models.expected b/tests/models/records/record2.models.expected new file mode 100644 index 000000000..d95838e69 --- /dev/null +++ b/tests/models/records/record2.models.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) +) diff --git a/tests/models/records/record2.models.smt2 b/tests/models/records/record2.models.smt2 new file mode 100644 index 000000000..1e4238645 --- /dev/null +++ b/tests/models/records/record2.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-datatype Pair +((pair (first Int) (second Int)))) +(declare-fun f (Int) Pair) +(assert (= (first (f 0)) 5)) +(check-sat) +(get-model) diff --git a/tests/models/records/record3.models.expected b/tests/models/records/record3.models.expected new file mode 100644 index 000000000..8b2d9f83a --- /dev/null +++ b/tests/models/records/record3.models.expected @@ -0,0 +1,7 @@ + +unknown +( + (define-fun x () Int 0) + (define-fun y () Int 5) + (define-fun f ((_arg_0 Int)) Pair (pair 5 0)) +) diff --git a/tests/models/records/record3.models.smt2 b/tests/models/records/record3.models.smt2 new file mode 100644 index 000000000..cc32e9e5b --- /dev/null +++ b/tests/models/records/record3.models.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-datatype Pair +((pair (first Int) (second Int)))) +(declare-fun f (Int) Pair) +(declare-const x Int) +(declare-const y Int) +(assert (= (first (f x)) 5)) +(assert (= (first (f 0)) y)) +(assert (= x 0)) +(check-sat) +(get-model) diff --git a/tests/models/uf/uf1.models.expected b/tests/models/uf/uf1.models.expected new file mode 100644 index 000000000..d3b170c21 --- /dev/null +++ b/tests/models/uf/uf1.models.expected @@ -0,0 +1,7 @@ + +unknown +( + (define-fun a () Int 0) + (define-fun b () Int 0) + (define-fun f ((_arg_0 Int)) Int 0) +) diff --git a/tests/models/uf/uf1.models.smt2 b/tests/models/uf/uf1.models.smt2 new file mode 100644 index 000000000..515bf7718 --- /dev/null +++ b/tests/models/uf/uf1.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-fun f (Int) Int) +(declare-const a Int) +(declare-const b Int) +(assert (= (f a) (f b))) +(check-sat) +(get-model) diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected new file mode 100644 index 000000000..232c59a45 --- /dev/null +++ b/tests/models/uf/uf2.models.expected @@ -0,0 +1,7 @@ + +unknown +( + (define-fun a () Int 0) + (define-fun b () Int (- 1)) + (define-fun f ((arg_0 Int)) Int (ite (= arg_0 0) 1 0)) +) diff --git a/tests/models/uf/uf2.models.smt2 b/tests/models/uf/uf2.models.smt2 new file mode 100644 index 000000000..42da76720 --- /dev/null +++ b/tests/models/uf/uf2.models.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-fun f (Int) Int) +(declare-const a Int) +(declare-const b Int) +(assert (distinct (f a) (f b))) +(check-sat) +(get-model) diff --git a/tests/quantifiers/testfile-trigger001.dolmen.expected b/tests/quantifiers/testfile-trigger001.dolmen.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/quantifiers/testfile-trigger001.dolmen.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/quantifiers/testfile-trigger001.cdcl.smt2 b/tests/quantifiers/testfile-trigger001.dolmen.smt2 similarity index 100% rename from tests/quantifiers/testfile-trigger001.cdcl.smt2 rename to tests/quantifiers/testfile-trigger001.dolmen.smt2 diff --git a/tests/quantifiers/testfile-trigger002.cdcl.ae b/tests/quantifiers/testfile-trigger002.dolmen.ae similarity index 100% rename from tests/quantifiers/testfile-trigger002.cdcl.ae rename to tests/quantifiers/testfile-trigger002.dolmen.ae diff --git a/tests/quantifiers/testfile-trigger002.dolmen.expected b/tests/quantifiers/testfile-trigger002.dolmen.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/quantifiers/testfile-trigger002.dolmen.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/quantifiers/testfile-trigger003.dolmen.expected b/tests/quantifiers/testfile-trigger003.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/quantifiers/testfile-trigger003.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/quantifiers/testfile-trigger003.dolmen.smt2 b/tests/quantifiers/testfile-trigger003.dolmen.smt2 new file mode 100644 index 000000000..37d5a1c09 --- /dev/null +++ b/tests/quantifiers/testfile-trigger003.dolmen.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL) +(declare-fun P (Int) Bool) +(declare-fun f (Int) Int) + +; This quantifier is explicitly annotated with a (f x) trigger. +; It should cause this problem to be unsat. +(assert + (forall ((x Int)) + (! (not (P x)) :pattern ((f x))))) + +; Use (f 0) +(assert (= (f 0) 0)) + +(assert (P 0)) + +(check-sat) diff --git a/tests/quantifiers/testfile-trigger004.dolmen.ae b/tests/quantifiers/testfile-trigger004.dolmen.ae new file mode 100644 index 000000000..2075c2b14 --- /dev/null +++ b/tests/quantifiers/testfile-trigger004.dolmen.ae @@ -0,0 +1,11 @@ +logic P : int -> bool +logic f : int -> int + +(* This quantifier is explicitly annotated with a f(x) trigger and should cause + the problem to be unsat *) +axiom trig : forall x : int [f(x)]. P(x) + +(* Use f(0) *) +axiom f_0 : f(0) = 0 + +goal g : P(0) diff --git a/tests/quantifiers/testfile-trigger004.dolmen.expected b/tests/quantifiers/testfile-trigger004.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/quantifiers/testfile-trigger004.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/smtlib/testfile-declare-datatype-incremental.dolmen.expected b/tests/smtlib/testfile-declare-datatype-incremental.dolmen.expected new file mode 100644 index 000000000..6f99ff0f4 --- /dev/null +++ b/tests/smtlib/testfile-declare-datatype-incremental.dolmen.expected @@ -0,0 +1,2 @@ + +unsat diff --git a/tests/smtlib/testfile-declare-datatype-incremental.cdcl.smt2 b/tests/smtlib/testfile-declare-datatype-incremental.dolmen.smt2 similarity index 100% rename from tests/smtlib/testfile-declare-datatype-incremental.cdcl.smt2 rename to tests/smtlib/testfile-declare-datatype-incremental.dolmen.smt2 diff --git a/tests/smtlib/testfile-echo1.dolmen.expected b/tests/smtlib/testfile-echo1.dolmen.expected new file mode 100644 index 000000000..8effb3e8c --- /dev/null +++ b/tests/smtlib/testfile-echo1.dolmen.expected @@ -0,0 +1 @@ +"Hello, world!" diff --git a/tests/smtlib/testfile-echo1.dolmen.smt2 b/tests/smtlib/testfile-echo1.dolmen.smt2 new file mode 100644 index 000000000..89c2f647e --- /dev/null +++ b/tests/smtlib/testfile-echo1.dolmen.smt2 @@ -0,0 +1,2 @@ +(set-logic ALL) +(echo "Hello, world!") \ No newline at end of file diff --git a/tests/smtlib/testfile-echo2.dolmen.expected b/tests/smtlib/testfile-echo2.dolmen.expected new file mode 100644 index 000000000..b4a2d7ebb --- /dev/null +++ b/tests/smtlib/testfile-echo2.dolmen.expected @@ -0,0 +1 @@ +"a""b" diff --git a/tests/smtlib/testfile-echo2.dolmen.smt2 b/tests/smtlib/testfile-echo2.dolmen.smt2 new file mode 100644 index 000000000..dec6f7933 --- /dev/null +++ b/tests/smtlib/testfile-echo2.dolmen.smt2 @@ -0,0 +1,2 @@ +(set-logic ALL) +(echo "a""b") \ No newline at end of file diff --git a/tests/smtlib/testfile-exit.dolmen.expected b/tests/smtlib/testfile-exit.dolmen.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/smtlib/testfile-exit.dolmen.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/smtlib/testfile-exit.dolmen.smt2 b/tests/smtlib/testfile-exit.dolmen.smt2 new file mode 100644 index 000000000..135ade6d3 --- /dev/null +++ b/tests/smtlib/testfile-exit.dolmen.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(check-sat) +(exit) +(check-sat) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-assignment1.err.dolmen.expected b/tests/smtlib/testfile-get-assignment1.err.dolmen.expected new file mode 100644 index 000000000..6cb130a54 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment1.err.dolmen.expected @@ -0,0 +1 @@ +(error "No model produced, cannot execute get-assignment.") diff --git a/tests/smtlib/testfile-get-assignment1.err.dolmen.smt2 b/tests/smtlib/testfile-get-assignment1.err.dolmen.smt2 new file mode 100644 index 000000000..2d8e91c82 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment1.err.dolmen.smt2 @@ -0,0 +1,3 @@ +(set-logic ALL) +; The next instruction should fail because we did not generate a model +(get-assignment) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-assignment2.err.dolmen.expected b/tests/smtlib/testfile-get-assignment2.err.dolmen.expected new file mode 100644 index 000000000..964245cf0 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment2.err.dolmen.expected @@ -0,0 +1,6 @@ + +unknown +( + (define-fun x () Int 0) +) +(error "Produce assignments disabled; add (set-option :produce-assignments true)") diff --git a/tests/smtlib/testfile-get-assignment2.err.dolmen.smt2 b/tests/smtlib/testfile-get-assignment2.err.dolmen.smt2 new file mode 100644 index 000000000..b5133db07 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment2.err.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const x Int) +(assert (! (= x 0) :named foo)) +(check-sat) +(get-model) +; The next instruction should fail because we did not activate the option +(get-assignment) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-assignment3.dolmen.expected b/tests/smtlib/testfile-get-assignment3.dolmen.expected new file mode 100644 index 000000000..a90ec1898 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment3.dolmen.expected @@ -0,0 +1,4 @@ + +unknown +((foo true)) + diff --git a/tests/smtlib/testfile-get-assignment3.dolmen.smt2 b/tests/smtlib/testfile-get-assignment3.dolmen.smt2 new file mode 100644 index 000000000..5aea879f7 --- /dev/null +++ b/tests/smtlib/testfile-get-assignment3.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-option :produce-assignments true) +(set-logic ALL) +(declare-const x Int) +(assert (! (= x 0) :named foo)) +(check-sat) +(get-assignment) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-info1.cdcl.expected b/tests/smtlib/testfile-get-info1.dolmen.expected similarity index 100% rename from tests/smtlib/testfile-get-info1.cdcl.expected rename to tests/smtlib/testfile-get-info1.dolmen.expected diff --git a/tests/smtlib/testfile-get-info1.cdcl.smt2 b/tests/smtlib/testfile-get-info1.dolmen.smt2 similarity index 100% rename from tests/smtlib/testfile-get-info1.cdcl.smt2 rename to tests/smtlib/testfile-get-info1.dolmen.smt2 diff --git a/tests/smtlib/testfile-get-info2.err.dolmen.expected b/tests/smtlib/testfile-get-info2.err.dolmen.expected new file mode 100644 index 000000000..2079d2e6f --- /dev/null +++ b/tests/smtlib/testfile-get-info2.err.dolmen.expected @@ -0,0 +1 @@ +(error "Invalid (get-info :reason-unknown)") diff --git a/tests/smtlib/testfile-get-info2.err.dolmen.smt2 b/tests/smtlib/testfile-get-info2.err.dolmen.smt2 new file mode 100644 index 000000000..9ae8a8ec5 --- /dev/null +++ b/tests/smtlib/testfile-get-info2.err.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) + +(declare-const x Int) + +(assert (= (* x x) 4)) + +(get-info :reason-unknown) +(check-sat) \ No newline at end of file diff --git a/tests/smtlib/testfile-get-info3.dolmen.expected b/tests/smtlib/testfile-get-info3.dolmen.expected new file mode 100644 index 000000000..ad7ccf7ad --- /dev/null +++ b/tests/smtlib/testfile-get-info3.dolmen.expected @@ -0,0 +1 @@ +unsupported diff --git a/tests/smtlib/testfile-get-info3.dolmen.smt2 b/tests/smtlib/testfile-get-info3.dolmen.smt2 new file mode 100644 index 000000000..7d60bad84 --- /dev/null +++ b/tests/smtlib/testfile-get-info3.dolmen.smt2 @@ -0,0 +1 @@ +(get-info :foo) \ No newline at end of file diff --git a/tests/smtlib/testfile-push-pop1.err.cdcl.expected b/tests/smtlib/testfile-push-pop1.err.dolmen.expected similarity index 100% rename from tests/smtlib/testfile-push-pop1.err.cdcl.expected rename to tests/smtlib/testfile-push-pop1.err.dolmen.expected diff --git a/tests/smtlib/testfile-push-pop1.err.cdcl.smt2 b/tests/smtlib/testfile-push-pop1.err.dolmen.smt2 similarity index 100% rename from tests/smtlib/testfile-push-pop1.err.cdcl.smt2 rename to tests/smtlib/testfile-push-pop1.err.dolmen.smt2 diff --git a/tests/smtlib/testfile-push-pop2.dolmen.expected b/tests/smtlib/testfile-push-pop2.dolmen.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/smtlib/testfile-push-pop2.dolmen.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/smtlib/testfile-push-pop2.cdcl.smt2 b/tests/smtlib/testfile-push-pop2.dolmen.smt2 similarity index 100% rename from tests/smtlib/testfile-push-pop2.cdcl.smt2 rename to tests/smtlib/testfile-push-pop2.dolmen.smt2 diff --git a/tests/smtlib/testfile-quoted1.dolmen.expected b/tests/smtlib/testfile-quoted1.dolmen.expected new file mode 100644 index 000000000..023946068 --- /dev/null +++ b/tests/smtlib/testfile-quoted1.dolmen.expected @@ -0,0 +1,5 @@ + +unknown +( + (define-fun |fail))| () Int 0) +) diff --git a/tests/smtlib/testfile-quoted1.dolmen.smt2 b/tests/smtlib/testfile-quoted1.dolmen.smt2 new file mode 100644 index 000000000..d171116c9 --- /dev/null +++ b/tests/smtlib/testfile-quoted1.dolmen.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-option :produce-models true) +(declare-const |fail))| Int) +(assert (= |fail))| 0)) +(check-sat) +(get-model) \ No newline at end of file diff --git a/tests/smtlib/testfile-reset.dolmen.expected b/tests/smtlib/testfile-reset.dolmen.expected new file mode 100644 index 000000000..76a9b3e2d --- /dev/null +++ b/tests/smtlib/testfile-reset.dolmen.expected @@ -0,0 +1,4 @@ + +unsat + +unknown diff --git a/tests/smtlib/testfile-reset.dolmen.smt2 b/tests/smtlib/testfile-reset.dolmen.smt2 new file mode 100644 index 000000000..101715c14 --- /dev/null +++ b/tests/smtlib/testfile-reset.dolmen.smt2 @@ -0,0 +1,8 @@ +(set-logic ALL) + +(declare-const b Bool) + +(assert (and b (not b))) +(check-sat) +(reset) +(check-sat) \ No newline at end of file diff --git a/tests/smtlib/testfile-steps-bound1.dolmen.err.expected b/tests/smtlib/testfile-steps-bound1.dolmen.err.expected new file mode 100644 index 000000000..4536febdd --- /dev/null +++ b/tests/smtlib/testfile-steps-bound1.dolmen.err.expected @@ -0,0 +1 @@ +(error "Invalid action during Assert mode: Set option steps_bound") diff --git a/tests/smtlib/testfile-steps-bound1.dolmen.err.smt2 b/tests/smtlib/testfile-steps-bound1.dolmen.err.smt2 new file mode 100644 index 000000000..2da3ac5d7 --- /dev/null +++ b/tests/smtlib/testfile-steps-bound1.dolmen.err.smt2 @@ -0,0 +1,7 @@ +(set-logic ALL) + +(declare-const x Int) +(assert (= (* x x) 3)) +(set-option :steps-bound 2) +; Should fail because this option cannot be set after set-logic +(check-sat) \ No newline at end of file diff --git a/tests/smtlib/testfile-steps-bound2.cdcl.expected b/tests/smtlib/testfile-steps-bound2.dolmen.expected similarity index 100% rename from tests/smtlib/testfile-steps-bound2.cdcl.expected rename to tests/smtlib/testfile-steps-bound2.dolmen.expected diff --git a/tests/smtlib/testfile-steps-bound2.cdcl.smt2 b/tests/smtlib/testfile-steps-bound2.dolmen.smt2 similarity index 100% rename from tests/smtlib/testfile-steps-bound2.cdcl.smt2 rename to tests/smtlib/testfile-steps-bound2.dolmen.smt2