Lab Exercise 2 CPP

launch.json

To enable debugging and running, switch your executable by setting the program and args fields as described here or follow the below screenshot.

Debugging

If you try to check the value of z3Expr, you can use to_string() to see the value. For example,

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

int main() {
    z3::context c;
    z3::expr x = c.int_const("x");
    z3::expr y = c.int_const("y");
    z3::expr formula = x > y;
    std::string expr_as_string = formula.to_string();
    std::cout << "The expression is: " << expr_as_string << std::endl;
    return 0;
}