Issue while creating model from scratch #7101
Description
Hi,
I'm trying to create a Z3::model given a set of equalities (variable == constant) that satisfy a formula. This doesn't always work, and I'm unsure if this is a bug or if I'm incorrectly using the API (4.12.4).
My first attempt was to assert the set of equalities in a z3::solver and generate a model (s.check(); s.get_model();). This approach always works without issues.
My second attempt aimed to make things faster by creating the model using the z3::model API without calling the solver. This approach fails in the following case, and I'm trying to figure out why.
The steps to reproduce the issue are:
- g++ main.cpp -lz3
- ./a.out formula.smt2 model.smt2
The steps above show how to reproduce the issue with the second approach (construct_model_fast). The formula is not evaluated as True by the model. Instead, it returns:
(let ((a!1 (fp.mul roundNearestTiesToEven
(fp.mul roundNearestTiesToEven
(fp.mul roundNearestTiesToEven
(fp #b0 #b10000000000 #x8000000000000)
(fp #b0 #b01010111111 #xfffffffff89ff))
(_ NaN 11 53))
(_ NaN 11 53))))
(let ((a!2 (fp.mul roundNearestTiesToEven
(fp.mul roundNearestTiesToEven
(fp.mul roundNearestTiesToEven
(fp #b0 #b01010111111 #xfffffffff89ff)
(_ NaN 11 53))
(_ NaN 11 53))
(fp.add roundNearestTiesToEven
(fp #b1 #b10000000010 #x4000000000000)
a!1))))
(let ((a!3 (= (_ NaN 11 53)
(fp.div roundNearestTiesToEven
(fp.mul roundNearestTiesToEven
(_ NaN 11 53)
(fp.add roundNearestTiesToEven
(fp #b0 #b10000000010 #xe000000000000)
a!2))
(fp #b0 #b10000000010 #x0000000000000)))))
(and a!3
(= (_ NaN 11 53)
(fp.mul roundNearestTiesToEven
(fp #b0 #b00000000000 #xc000000000009)
(_ NaN 11 53)))))))
However, if construct_model_slow is used, the model correctly evaluates the formula as True.
Best,
Manuel.