Possible issue with And operation between 'zext' and 'const' expr?

[Hanseltu]

Hi,

Please consider the following source file test.cc which uses z3 APIs,

#include "z3++.h"
using namespace z3;

int main(){
    context c;
    expr zz = c.bv_const("zz", 16);
    expr const_test1 = c.bv_val(0x8000000, 32);
    expr zeroext = zext(zz, 32);
    std::cout << "zeroext : " << zeroext << std::endl;
    expr and_test = zeroext & const_test1; // not work
    // expr and_test = zeroext & 0x8000000; // works well
    std::cout << "and_test : " << and_test<< std::endl;
    return 0;
}

I compiled it with g++ test.cc -lz3 -L./z3/ -I./z3/include -o test, and I got the following when I execute the ./test:

zeroext : ((_ zero_extend 32) zz)
and_test : null

I got a null expression as z3 reported. However, when I replaced the line expr and_test = zeroext & const_test1; with expr and_test = zeroext & 0x8000000;, I got the expected outputs:

zeroext : ((_ zero_extend 32) zz)
and_test : (bvand ((_ zero_extend 32) zz) #x000008000000)

The z3 version I used is Z3 version 4.8.14 - 64 bit.

Is it a possible issue in z3, or did I miss anything here? Thank you very much for your help.

Best,
Haoxin

[NikolajBjorner]

The two expressions zeroext and const_test1 have different bit-widths, zeroext has bit-width 48, while onst_test1 has width 32.
This is a type error that the C++ interface silently ignores. I have updated z3++.h to include error checking at places I saw them missing. Your program will now "crash" with an exception

int main(){
    context c;
    try {
        expr zz = c.bv_const("zz", 16);
        expr const_test1 = c.bv_val(0x8000000, 32);
        expr zeroext = zext(zz, 32);
        std::cout << "zeroext : " << zeroext << std::endl;
        expr and_test = zeroext & const_test1; // not work
        // expr and_test = zeroext & 0x8000000; // works well
        std::cout << "and_test : " << and_test<< std::endl;
    }
    catch (exception& ex) {
        std::cout << ex << "\n";
    }
    return 0;
}

prints

Argument #x08000000 at position 1 has sort (_ BitVec 32) it does does not match declaration (declare-fun bvand ((_ BitVec 48) (_ BitVec 48)) (_ BitVec 48))