I have this c++ code that uses z3 operators.
std::vector<z3::expr> bv_vector_immediate = {};
int immediate_int = immediates[0]->get_immediate_value_int();
bv_vector_immediate.push_back(z3_ctx.bv_val(immediate_int, 64));
Z3_LHS = get_register_value(register1).back(); //bv_val(0, 64)
Z3_RHS = bv_vector_immediate.back(); //bv_val(10, 64)
output = z3::operator-(Z3_LHS,Z3_RHS);
std::cout << z3_solver.check() << "\n";
z3::model m = z3_solver.get_model();
bv_vector_output.push_back(m.eval(output));
std::cout << Z3_LHS << "-" << Z3_RHS << " = " << m.eval(output).get_numeral_int64() << std::endl;
the output I get is:
terminate called after throwing an instance of 'z3::exception'
Aborted (core dumped)
however when I change the operator to + by changing this line here, the code works normally.
output = z3::operator+(Z3_LHS,Z3_RHS);
I believe since the result of the - operation yields a negative value, some z3 exception is thrown at the last line std::cout << Z3_LHS << "-" << Z3_RHS << " = " << m.eval(output).get_numeral_int64() << std::endl;. So how can I get around this issue of getting numeral int representation of a z3 expression resulting from a large bit vector value being subtracted from a smaller bit vector value. I could only find those z3 functions to get int representation of a bitvector value z3 expression : get_numeral_int64, get_numeral_uint64, get_numeral_int, get_numeral_uint.
Please always post reproducible code segments. Just posting "parts" of your code makes it very difficult for others to diagnose the problem.
Having said that, your problem is that the value 0-10 does not fit in an int64 value as a bit-vector. Here's a minimal reproducer:
#include <z3++.h>
using namespace z3;
using namespace std;
int main ()
{
context c;
expr lhs = c.bv_val( 0, 64);
expr rhs = c.bv_val(10, 64);
expr output = lhs - rhs;
solver s(c);
cout << s.check() << endl;
model m = s.get_model();
cout << m.eval(output).get_numeral_int64() << endl;
return 0;
};
When I run this, I get:
$ g++ -std=c++11 a.cpp -l z3
$ ./a.out
sat
libc++abi: terminating with uncaught exception of type z3::exception
You might ask why this is the case? The result, after all is 0-10, i.e., -10, which can very well fit in a 64-bit bit-vector. But recall that bitvector arithmetic has no notion of signs; it's the operations that do signed arithmetic. So, in 64-bit arithmetic -10 actually is the same value as 18446744073709551606, which indeed does not fit in the range of an int64, whose maximum value is 9223372036854775807.
How do you fix this? Well, it really depends on how you want to treat these bit vector values. I'm assuming you want to treat these as signed integer values. Then, in the reproducer above, change the last line to:
cout << (int64_t) m.eval(output).get_numeral_uint64() << endl;
When I run it like this, I get:
sat
-10
which is probably what you wanted.
Summary In z3, Bit-vector values have no sign associated with them. They are just a bunch of bits. But when you do operations on them, you need to be careful on choosing the correct signed/unsigned operation. (Note that for some operations like addition/subtraction it's the same operation; but for others, such as comparisons and extraction of values, you have to pay special attention to signs.) You might want to review http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml for which operations need to be careful about signs. Rule-of-thumb: Extraction of actual values in a model will always have to pay attention to the signedness.
Side note I'd further argue that this is actually a shortcoming of the C++ API for z3. A higher-level API can actually keep track of signedness and use the correct operations for you automatically without the end-user having the keep track of the same. Unfortunately the C/C++ API is not that high-level. But that's a discussion for a different day.