mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-29 11:58:51 +00:00
Code Activity

Clarify BV SMT2 regression assertion

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-18 19:24:44 +00:00 • committed by GitHub
parent 586a6b893d
commit f8ba42c5c4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/test/api.cpp
View file

@ -99,6 +99,7 @@ void test_bvneg() {
Z3_solver_push(ctx, s); Z3_solver_push(ctx, s);
Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, sx, minus_one)); Z3_solver_assert(ctx, s, Z3_mk_eq(ctx, sx, minus_one));
std::string smt2 = Z3_solver_to_string(ctx, s); std::string smt2 = Z3_solver_to_string(ctx, s);
// Bit-vector numerals must print in canonical unsigned SMT2 form.
ENSURE(smt2.find("(_ bv-") == std::string::npos); ENSURE(smt2.find("(_ bv-") == std::string::npos);
Z3_solver_pop(ctx, s, 1); Z3_solver_pop(ctx, s, 1);
} }