Basile Clément 05b2d1650d fix(CP): Make sure domains do not overflow the default domain (#1225) ...

* fix(CP): Make sure domains do not overflow the default domain

When reading domains through a non-canonical representative, we are
intersecting it with the default domain of the representative (i.e. the
range of the bit-vector type) in order to ensure that the resulting
domain is known to be within the range of the type.

This is useful for interval domains because we keep track of global
bounds, which we rely on in functions such as [bvshl], but are forgotten
by the call to [add_explanation].

We also need to perform the same intersection when modifying a domain
through a non-canonical representative, otherwise we might store a
domain that overflows the bounds of the type.

(It is unfortunate that we have to do this dance instead of storing type
information on the interval themselves, but that would be a bigger change).

This was found by fuzzing.

* Clarify doc

2024-08-29 12:08:42 +02:00

..

bitlist-interval001.expected

feat(BV): Interval domains for bit-vectors (#1058)

2024-06-21 10:02:57 +02:00

bitlist-interval001.smt2

feat(BV): Interval domains for bit-vectors (#1058)

2024-06-21 10:02:57 +02:00

testfile-array-cs.dolmen.expected

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-array-cs.dolmen.smt2

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-bitv001.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv001.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv002.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv002.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv003.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv003.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv004.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv004.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv005.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv005.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv006.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv006.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv007.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv007.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv008.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv008.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv009.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv009.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv010.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv010.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv011.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv011.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv012.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv012.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv013.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv013.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv014.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv014.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv015.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv015.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv016.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv016.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv017.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv017.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv018.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv018.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv019.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv019.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv020.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv020.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv021.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv021.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv022.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv022.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv023.ae

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv023.expected

Fix ci (#535)

2022-11-28 10:29:31 +01:00

testfile-bitv024.expected

fix: Do not call [X.make] on non-subterms for bv2nat (#954)

2023-11-22 09:19:25 +01:00

testfile-bitv024.smt2

fix: Do not call [X.make] on non-subterms for bv2nat (#954)

2023-11-22 09:19:25 +01:00

testfile-bitv025.expected

fix(BV): Do not call [X.make] on non-subterm, reloaded (#969)

2023-11-24 15:56:19 +00:00

testfile-bitv025.smt2

fix(BV): Do not call [X.make] on non-subterm, reloaded (#969)

2023-11-24 15:56:19 +00:00

testfile-bitv026.expected

fix(BV): Apply C-substitutions recursively (#978)

2023-11-27 13:50:57 +01:00

testfile-bitv026.smt2

fix(BV): Apply C-substitutions recursively (#978)

2023-11-27 13:50:57 +01:00

testfile-bitv027.expected

fix(BV): Allow substituting constants (#979)

2023-11-27 13:08:12 +00:00

testfile-bitv027.smt2

fix(BV): Allow substituting constants (#979)

2023-11-27 13:08:12 +00:00

testfile-bv2nat-001.expected

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-001.smt2

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-002.expected

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-002.smt2

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-003.expected

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-003.smt2

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-004.expected

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-004.smt2

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-005.expected

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-005.smt2

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-006.expected

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-006.smt2

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-007.expected

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-007.smt2

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-009.expected

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-009.smt2

feat(BV): Add support for bv2nat/int2bv normal forms (#1154)

2024-08-20 11:55:03 +02:00

testfile-bv2nat-delayed.dolmen.expected

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-bv2nat-delayed.dolmen.smt2

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-bv2nat-immediate.dolmen.expected

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-bv2nat-immediate.dolmen.smt2

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-bv2nat-models.dolmen.expected

feat(BV): Display BV constants using hexadecimal (#1082)

2024-03-29 17:51:59 +01:00

testfile-bv2nat-models.dolmen.smt2

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-bvadd-001.dolmen.expected

feat(BV, CP): Add bitlist propagators for add/sub (#1151)

2024-07-22 16:00:49 +02:00

testfile-bvadd-001.dolmen.smt2

feat(BV, CP): Add bitlist propagators for add/sub (#1151)

2024-07-22 16:00:49 +02:00

testfile-bvadd-002.dolmen.expected

feat(BV, CP): Add bitlist propagators for add/sub (#1151)

2024-07-22 16:00:49 +02:00

testfile-bvadd-002.dolmen.smt2

feat(BV, CP): Add bitlist propagators for add/sub (#1151)

2024-07-22 16:00:49 +02:00

testfile-bvand-001.dolmen.expected

feat(BV): Word-level propagation for BV logic (#944)

2023-11-30 16:40:35 +00:00

testfile-bvand-001.dolmen.smt2

feat(BV): Word-level propagation for BV logic (#944)

2023-11-30 16:40:35 +00:00

testfile-bvnot-term.dolmen.expected

Do not discard bvnot applied to uninterpreted terms (#819)

2023-09-14 16:41:08 +02:00

testfile-bvnot-term.dolmen.smt2

Do not discard bvnot applied to uninterpreted terms (#819)

2023-09-14 16:41:08 +02:00

testfile-bvnot.dolmen.expected

Partial support of the primitive bvnot (#745)

2023-07-25 16:46:44 +02:00

testfile-bvnot.dolmen.smt2

Partial support of the primitive bvnot (#745)

2023-07-25 16:46:44 +02:00

testfile-bvor-001.dolmen.expected

feat(BV): Word-level propagation for BV logic (#944)

2023-11-30 16:40:35 +00:00

testfile-bvor-001.dolmen.smt2

feat(BV): Word-level propagation for BV logic (#944)

2023-11-30 16:40:35 +00:00

testfile-bvshl-001.expected

fix(CP): Make sure domains do not overflow the default domain (#1225)

2024-08-29 12:08:42 +02:00

testfile-bvshl-001.smt2

fix(CP): Make sure domains do not overflow the default domain (#1225)

2024-08-29 12:08:42 +02:00

testfile-bvshl-002.expected

fix(CP): Make sure domains do not overflow the default domain (#1225)

2024-08-29 12:08:42 +02:00

testfile-bvshl-002.smt2

fix(CP): Make sure domains do not overflow the default domain (#1225)

2024-08-29 12:08:42 +02:00

testfile-bvsub-001.dolmen.expected

feat(BV, CP): Add bitlist propagators for add/sub (#1151)

2024-07-22 16:00:49 +02:00

testfile-bvsub-001.dolmen.smt2

feat(BV, CP): Add bitlist propagators for add/sub (#1151)

2024-07-22 16:00:49 +02:00

testfile-bvsub-002.dolmen.expected

feat(BV, CP): Add bitlist propagators for add/sub (#1151)

2024-07-22 16:00:49 +02:00

testfile-bvsub-002.dolmen.smt2

feat(BV, CP): Add bitlist propagators for add/sub (#1151)

2024-07-22 16:00:49 +02:00

testfile-bvxor-001.dolmen.expected

feat(BV): Word-level propagation for BV logic (#944)

2023-11-30 16:40:35 +00:00

testfile-bvxor-001.dolmen.smt2

feat(BV): Word-level propagation for BV logic (#944)

2023-11-30 16:40:35 +00:00

testfile-int2bv-delayed.dolmen.expected

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-int2bv-delayed.dolmen.smt2

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-int2bv-immediate.dolmen.expected

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-int2bv-immediate.dolmen.smt2

Support delayed computation of partially interpreted functions (#869)

2023-10-12 16:41:28 +02:00

testfile-qfbv-timeout.unix.dolmen.expected

Restore Windows CI on Cygwin (#1203)

2024-08-09 14:46:35 +02:00

testfile-qfbv-timeout.unix.dolmen.smt2

Restore Windows CI on Cygwin (#1203)

2024-08-09 14:46:35 +02:00

testfile-repeat-001.expected

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-repeat-001.smt2

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-repeat-002.expected

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-repeat-002.smt2

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-sign-extend-001.expected

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-sign-extend-001.smt2

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-sign-extend-002.expected

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-sign-extend-002.smt2

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-sign-extend-003.expected

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-sign-extend-003.smt2

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-sign-extend-004.expected

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00

testfile-sign-extend-004.smt2

fix(BV): Internalize sign_extend and repeat (#1192)

2024-08-19 07:46:00 +00:00