Solver printing wrong model in C++ api

[anirjoshi]

Hello, I have the following code in which the solver always seems to print the first model.

#include <iostream>
#include "z3++.h"

using namespace z3;

int main() {
    // Initialize the Z3 context
    context c;

    solver s(c);

    // Define some variables
    expr x = c.real_const("x");
    expr y = c.real_const("y");

    // Add some constraints
    s.add(x + y > 10);
    s.add(x > 1);
    s.add(y > 1);
    std::cout << s << std::endl;;
    std::cout << s.check() << " " << s.get_model() << std::endl;
    std::cout << s << std::endl;

    std::cout << "---------adding constraint x<5----------------\n";
    s.add(x<5);
    std::cout << s.check() << " " << s.get_model()<< std::endl;
    std::cout << s << std::endl;
}

In the output, even after the second s.check() call the std::cout << s << std::endl; prints the model corresponding to the first s.get_model(). Note that the second s.get_model() prints the correct model, i.e, it changes the model because of the added constraint (as expected), but this change is not reflected in the last statement std::cout << s << std::endl;.

[NikolajBjorner]

You have to pay attention to evaluation order in C/C++. Rewrite the pipe that prints to std::out to finish first the check before printing the model.

#include <iostream>
#include "z3++.h"

using namespace z3;

int main() {
    // Initialize the Z3 context
    context c;

    solver s(c);

    // Define some variables
    expr x = c.real_const("x");
    expr y = c.real_const("y");

    // Add some constraints
    s.add(x + y > 10);
    s.add(x > 1);
    s.add(y > 1);
    std::cout << s << std::endl;;
    std::cout << s.check() << " ";
    std::cout << s.get_model() << std::endl;
    std::cout << s << std::endl;

    std::cout << "---------adding constraint x<5----------------\n";
    s.add(x<5);
    std::cout << s.check() << " ";
    std::cout << s.get_model()<< std::endl;
    std::cout << s << std::endl;
}

C:\z3\build>pm.exe
(declare-fun y () Real)
(declare-fun x () Real)
(assert (> (+ x y) 10.0))
(assert (> x 1.0))
(assert (> y 1.0))

sat (define-fun y () Real
  2.0)
(define-fun x () Real
  9.0)
(declare-fun y () Real)
(declare-fun x () Real)
(assert (> (+ x y) 10.0))
(assert (> x 1.0))
(assert (> y 1.0))
(model-add y () Real 2.0)
(model-add x () Real 9.0)

---------adding constraint x<5----------------
sat (define-fun y () Real
  7.0)
(define-fun x () Real
  4.0)
(declare-fun y () Real)
(declare-fun x () Real)
(assert (> (+ x y) 10.0))
(assert (> x 1.0))
(assert (> y 1.0))
(assert (< x 5.0))
(model-add y () Real 2.0)
(model-add x () Real 9.0)

The model ses x to 4 in the second call.