mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 14:56:11 +00:00
Code Activity

change unit test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-20 13:57:19 -07:00
parent baa66c3a8a
commit b9cc87ae4b
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/test/seq_rewriter.cpp
View file

@ -135,7 +135,7 @@ void tst_seq_rewriter() {
} }
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------
// 10. Range complement (lo = 0): single range [hi+1, max] // 10. Range complement (lo = 0): single range e union [hi+1, max].*
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------
{ {
expr_ref lo_str(su.str.mk_string(zstring(0u)), m); expr_ref lo_str(su.str.mk_string(zstring(0u)), m);
@ -144,7 +144,6 @@ void tst_seq_rewriter() {
rw(e); rw(e);
std::cout << "range comp lo=min: " << mk_pp(e, m) << "\n"; std::cout << "range comp lo=min: " << mk_pp(e, m) << "\n";
ENSURE(!su.re.is_complement(e)); ENSURE(!su.re.is_complement(e));
ENSURE(su.re.is_range(e));
} }
// ----------------------------------------------------------------------- // -----------------------------------------------------------------------