extracting value from a model in exists_expr_vector_example

Question

In the exists_expr_vector_example() function from the file example.cpp, when I am trying to extract a value of a variable, say xs[1], using the code:

    solver s(c);
    s.add(ex); s.check();
    model m = s.get_model();
    cout<<m.eval(xs[1]);

I am getting an output of x_1, instead of the value of the variable x_1. How should we approach this problem.

Answer 1

In the exists example, the variables are bound. You can assert 'b' instead of 'ex'. In 'b', the variables in xs are not bound and the model will assign values for free variables. Models do not assign values for bound variables.

solver s(c);
s.add(b); s.check();
model m = s.get_model();
std::cout<<m.eval(xs[1]) << "\n";