printing models

[ozan....@gmail.com]

Hi,

My configuration file contains the following line for printing the models:

produce_models 1

However, in some problem instances only some parts of the models are printed. For example, consider the following SMT file:

***

(set-logic QF_UF)

(declare-fun x () Bool)

(declare-fun y () Bool)

(assert (or x y))

(check-sat)

(exit)

***

opensmt outputs only "sat" for this instance and does not print any models. However, when we add the following clause:

(assert (or (not x) y))

The output is now:

y

sat

How can you explain this behaviour? I have experimented with bigger instances too, where only a (possibly empty) subset of the variables is shown in the output.

Thanks,

Ozan

[Robert White]

Hi, 

I am using the API but I can't print the model or proof. Is that the reason why?

Can anyone print the model????

Thanks
Robert White

[Robert White]

I think I got it. Its just a typo.

Sorry.