Unknown solution when multiplied by one

[anirjoshi]

Hello, I have the following program that returns sat correctly:

#include <iostream>
#include <sstream>
#include<vector>
#include"z3++.h"
using namespace z3;

int main() {
    z3::config cfg;
    cfg.set("auto_config",true);
    z3::context c(cfg);
    z3::solver s = z3::tactic(c, "smt").mk_solver();
    s.set("smt.arith.nl.nra", false);

    z3::expr x = c.real_const("x");
    z3::expr y = c.real_const("y");
    z3::expr ct = c.real_const("c");

    z3::expr mt = c.real_val("-2");
    z3::expr one = c.real_val("1");

    z3::expr const1 =  (x*x)+(y*ct);
    z3::expr const2 =  (x)-(y*y)*ct+ct;

    s.add(const1<c.real_val("0"));
    s.add(const2<c.real_val("0"));

    std::cout << s.check() << std::endl;

    return 0;
}

But when I change one line defining const1, to z3::expr const1 = (x*x)+(one*y*ct);, I get an unknown. How to resolve this? I have a program that is using z3 solver internally and has a lot of such one multiplication terms. Is it because of this multiplication one terms that the solver returns unknown? How to resolve this issue?

The program that gives an unknown solution is:

#include <iostream>
#include <sstream>
#include<vector>
#include"z3++.h"
using namespace z3;

int main() {
    z3::config cfg;
    cfg.set("auto_config",true);
    z3::context c(cfg);
    z3::solver s = z3::tactic(c, "smt").mk_solver();
    s.set("smt.arith.nl.nra", false);

    z3::expr x = c.real_const("x");
    z3::expr y = c.real_const("y");
    z3::expr ct = c.real_const("c");

    z3::expr mt = c.real_val("-2");
    z3::expr one = c.real_val("1");

    z3::expr const1 =  (x*x)+(one*y*ct);
    z3::expr const2 =  (x)-(y*y)*ct+ct;

    s.add(const1<c.real_val("0"));
    s.add(const2<c.real_val("0"));

    std::cout << s.check() << std::endl;

    return 0;
}

Thank You!

[NikolajBjorner]

use the nlsat tactic.