Several problems with SmtSymbols.transferSymbols

ultimate-pa / ultimate

The Ultimate program analysis framework.

https://ultimate-pa.org/

197 stars 41 forks source link

Several problems with SmtSymbols.transferSymbols #442

Open Heizmann opened 5 years ago

Heizmann commented 5 years ago

I get de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Quantifier not supported. If this is solved there seems to be the more difficult problem that symbols are declared twice.

trunk/examples/settings/default/automizer/svcomp-Reach-64bit-Automizer_Default.epf trunk/examples/programs/regression/bpl/TestFunctionWithBody.bpl trunk/examples/toolchains/AutomizerBpl.xml

Heizmann commented 5 years ago

I have the impression that transferring symbols eagerly is incompatible to the idea of the TermTransferrer

danieldietsch commented 5 years ago

From my POV, SmtSymbols works as intended. The term is only transferred during the creation of a new script.

The exception is to be expected, because the example in question contains a function without the attribute { :inline true }, so that an axiom with forall quantifier is added. SmtInterpol crashes when this quantified axiom is asserted. If you add the attribute to the function, everything works as expected (the function gets inlined and no axiom is created)

Before the introduction of SmtSymbols we did not assert axioms (which was a bug).

EDIT: SmtSymbols uses TermTransferrer to translate the terms.

Heizmann commented 5 years ago

Nice, but what about the cases in the user does not want to inline the function?

Am I right that your finding is the following

The example was put in the wrong folder and should (quantifiers!) be moved to trunk/examples/programs/quantifier/regression/bpl/
There is a problem with the refinement engine: It seems like all refinement strategies that use SMTInterpol cannot handle Boogie programs with axioms.
The (second) bug that symbols are declared twice cannot be reproduced if you inline the function.

I definitely agree with 1. and 2. I will try to find an example that allow us to reproduces the declare-twice-bug. But while doing so I stumbled upon another bug: it seems like there is a bug for functions with zero parameters (see #443 ).

Heizmann commented 5 years ago

By the way: I am perfectly happy if we do not yet address 2. (refinement engine) now.

Heizmann commented 5 years ago

You should be able to reproduce the "declare-twice-bug" if you use the following settings. trunk/examples/settings/automizer/interpolation/Reach-32bit-Z3-IcSpLv.epf

The error message is de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Function myIncrement is already defined.

Heizmann commented 5 years ago

I think I know the problem:

The SmtSymbols.transferSymbols uses the TermTransferrer to transfer the axiom.
The TermTransferrer declares the required function symbols on-demand.
Afterwards SmtSymbols.transferSymbols declares all function symbols eagerly. (Already declared symbols are declared twice)

A quick workaround would be to swap the translation of the axiom and the eager declaration of function symbols. However, there are more issues. I1 SmtSymbols.transferSymbols re-implements features of the TermTransferrer and we should avoid this. I2 The name "transferSymbols" is misleading since it also transfers the axioms, axioms are also missing in the documentation. I3 The following line is questionable. I think inconsistent axioms are legal. assert quickCheckAxioms != LBool.UNSAT : "Axioms are inconsistent";

Do we have code that really needs a feature of SmtSymbols.transferSymbols but the transfer of the axioms?

Heizmann commented 5 years ago

Added issue #443 for one of the above mentioned problems.