Conceptual problem in DiffWrapperScript

[Heizmann]

If the DiffWrapperScript see a term in which there is a quantified variable inside the @diff function (e.g., (and (< |c_#StackHeapBarrier| |c_ULTIMATE.start_main_~#s~0#1.base|) (exists ((|v_#length_BEFORE_CALL_4| (Array Int Int))) (let ((.cse0 (@diff |v_#length_BEFORE_CALL_4| |c_#length|))) (and (<= 4 (select |v_#length_BEFORE_CALL_4| |c_ULTIMATE.start_main_~#s~0#1.base|)) (or (= |c_#length| |v_#length_BEFORE_CALL_4|) (<= (+ .cse0 1) |c_#StackHeapBarrier|)) (= |c_#length| (store |v_#length_BEFORE_CALL_4| .cse0 (select |c_#length| .cse0)))))) (= |c_ULTIMATE.start_main_~#s~0#1.offset| 0)) it asserts an axiom (e.g., (=> (let ((.cse0 (ULTIMATE@diffIntInt |v_#length_BEFORE_CALL_4| |c_#length|))) (= (select |v_#length_BEFORE_CALL_4| .cse0) (select |c_#length| .cse0))) (= |v_#length_BEFORE_CALL_4| |c_#length|)) that contains all subterms of the @diff function. Hence the axiom is not a closed formula and the SMT solver cannot assert the axiom. (The axiom does not make sense at all.)

A typical error message is Interpolation failed due to KNOWN_DEPENDING: line 54101 column 46: unknown constant v_#length_BEFORE_CALL_2.
In a 90s SV-COMP run that compared two settings the problem occurred 55 times.

One example is ./Ultimate.py --spec ../sv-benchmarks/c/properties/valid-memsafety.prp --file ../sv-benchmarks/c/list-simple/sll2c_remove_all.i --full-output --architecture 32bit.

[danieldietsch]

Perhaps @jhoenicke has an idea for that.

[jhoenicke]

The problem is that it wasn't designed for quantifiers. There are several solutions:

1. If quantifiers are enabled, just add the axiom (forall (a (Array..)) (b (Array ..)) (=> (= (select a (diff a b)) (select b (diff a b))) (= a b))) and don't add any other axiom.
2. like 1. but add the instantiated axioms that don't involve variables (to help the solver a bit)
3. add forall quantifiers around the axioms that involve variables.
4. add the axiom in the same scope as the variable.

Option 4. is tricky as you have to determine whether the quantifier occurs positive or negative and doesn't work, if it occurs in the condition of an ite. I'm leaning towards solution 3, as it seems a simple enough change (just add universal quantifiers).

[Heizmann]

I don't understand solution 3. Do you suggest that we add two kinds of axioms?
One kind of axiom for formulas with quantified variables, the other kind of axiom for formulas without quantified variables?
The I don't see why this is simple. How do you know which variables are quantified? How do you determine the scope in which these variables occur? You would need some lookahead while processing a formula. If you have to do a lookahead anyway, solution 4. is not significantly more difficult than solution 3.

[jhoenicke]

The solution 3. would be to build the axiom, then check if it has free variables (Term.getFreeVariables()), and if that returns a non-empty array, add a forall quantifier around it.

[Heizmann]

I don't understand your fix. Let's assume I call DiffWrapperScript#convertApplicationTerm on a term (@diff t1 t2) where t1 has a free variable x. Now, what should this method do?

[jhoenicke]

In checkOrAddAxiom before assertTerm(axiom) (here) insert something like:

TermVariable[] tvs = axiom.getFreeVars();
if (tvs.length > 0) {
   axiom = quantifier(Script.FORALL, tvs, axiom);
}

[maul-esel]

Closing this issue, as was clearly intended in 5a329ed.