how to get integer value of a z3 expression in c++

Question

I have this piece of code here that adds two z3 bit-vector values in c++

expr Z3_LHS=z3_ctx.bv_val(0, 64);
expr Z3_RHS=z3_ctx.bv_val(8, 64);
output=Z3_LHS+Z3_RHS;

when I print the output I get

bvadd #x0000000000000000 #x0000000000000008

Please how can I get the integer value of this output expression which should be 8 instead of this long line. In other words I want to evaluate this expression to an integer value.

Answer 1

This is a bit of an odd thing to do, since you wouldn't use z3 to add constant numbers. But, here's how you'd code what you want using the C++ api:

#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(8, 64);
  expr out = lhs+rhs;

  solver s(c);
  cout << s.check() << "\n";
  model m = s.get_model();
  cout << m.eval(out).get_numeral_int64() << "\n";

  return 0;
};

Assuming you put this in a file named a.cpp, here's what I get:

$ g++ -std=c++11 a.cpp -l z3
$ ./a.out
sat
8