I was wondering why the following AST is unsat:
(= (extract 31 0 (sign_extend 32 -5)) -5)
-5 has a bitvector type of size 32, which is then sign extended it to a bitvector of size 64 and then the 32 lower bits are extracted. I thought that the resulting bitvector should be equal to the original bitvector.Note that this example returns sat for positive bitvectors.
I am trying to add support for casts from signed 32 bit integers to signed 64 bit integers and vice versa. Neither conversion seems to work.
The following code illustrates my problem. It sign extends a 32 bit bitvector constant to a 64 bit vector. However, the resulting bitvector does not appear to be equal to the 64 bitvector constant initialized to hold the same constant value. If I change the constant to a positive value, then the resulting set of constraints is satisfiable.
This problem also occurs (the commented code) when the lowest 32 bits are extracted from a 64 bitvector constant.
#include<stdio.h>#include<z3.h>int main(void) { Z3_config cfg; Z3_context ctx; cfg = Z3_mk_config(); Z3_set_param_value(cfg, "MODEL", "true"); ctx = Z3_mk_context(cfg); Z3_enable_bv(ctx); Z3_type_ast int32_type = Z3_mk_bv_type(ctx, 32); Z3_type_ast int64_type = Z3_mk_bv_type(ctx, 64); Z3_ast int32_const = Z3_mk_int(ctx, -5, int32_type); Z3_ast int64_const = Z3_mk_int(ctx, -5, int64_type); Z3_ast int32_to_int64 = Z3_mk_sign_ext(ctx, 32, int32_const); Z3_ast cmp = Z3_mk_eq(ctx, int64_const, int32_to_int64); //Z3_ast int64_to_int32 = Z3_mk_extract(ctx, 31, 0, int64_const); //Z3_ast cmp = Z3_mk_eq(ctx, int32_const, int64_to_int32); Z3_assert_cnstr(ctx, cmp); Z3_model m = 0; Z3_lbool result = Z3_check_and_get_model(ctx, &m); printf("sat: %d", result); if(m) { printf("\n%s\n", Z3_model_to_string(ctx, m)); } Z3_del_context(ctx); Z3_del_config(cfg);}
Does anybody have any ideas?
I have been investigating this problem further. It appears that bitvectors of a size of 30 bits and more, cause Z3 to calculate the wrong answer.
Consider the following AST where -1, 0 and k!0 are bitvectors of size 29:
(= -1 (bvadd 0 k!0))
Solving it, results in the following model:
partitions:*2 {k!0} -> 536870911:bv29
Note that in this case we get the right result: 536870911 = 11111111111111111111111111111 = -1
Increasing the bitvector size to 30 causes my C application to return unsat.
This problem also occurs when all the bitvectors need to be positive.
Consider the following AST where 0, 1073741822 and k!0 are bitvectors of size 32:
(= k!0 (bvadd 0 1073741822))
partitions:*2 {k!0} -> 1073741822:bv32
1073741822 = 111111111111111111111111111110 = 2^30 -2 = MAX_SIGNED_INTEGER_32_VALUE / 2 -1
However, when I increase the value by one (1073741823) then again Z3 fails.
I am currently using Z3 version 1.3.6 debug, this problem also seems to appear on Z3 version 1.2.
Hope to hear from you soon...
Thanks for the detailed investigation. We are currently preparing Z3 v2 for release, and I will check your findings with it.
Generally speaking, bit-vectors are neither signed nor unsigned. There is signed comparison and signed division operators, on the other hand.The conversion of unsigned numbers to bit-vectors is well defined as just the bit-pattern of the unsigned number. The conversion of signed numbers to bit-vectors is done in a couple of places in 1.3 and it is likely ambiguous.I therefore suggest you use unsigned numbers for now when creating bit-vectors.
I just wanted to inform you, that this problem does not occur anymore when I switched over to Z3 2.0. Thanks, for the new release.
You are very welcome. Yes, I made sure to check this. :-), but did not back-port fixes to v1.