search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

Why isn't model_validate=true the default? #3398

Closed copumpkin closed 4 years ago

copumpkin commented 4 years ago

I'm tempted to turn it on for all my z3 usage and I'm wondering why it isn't the default. Is it expensive or are there other downsides I'm not seeing? Intuitively it doesn't seem like it would be expensive, but I'm wary of "going against the grain" if there were good reasons for existing defaults.

NikolajBjorner commented 4 years ago

It is incomplete, so could give false positives. I don't want to support it as a feature when it is known to provide false positives in some corner cases. There are too many "support calls" on similar false alarms already and it takes a lot of time weeding out what matters from what doesn't.

For most uses it is accurate. We use model_validate=true for all regressions against SMTLIB.

If you find false positives in model_validate you are of course welcome to fix them.

copumpkin commented 4 years ago

Ah, thank you, that makes sense!