The deduction using Octagon domain can not return relevant meet irreducibles.
Consider a program below:
int main() {
unsigned x, y;
__CPROVER_assume(x==y);
x++; y++;
x++; y++;
assert(x==y);
}

Using Interproc analyzer with forward analysis and octagon domain, the following annotated code
is obtained :
Annotated program after forward analysis
var x : int, y : int;
begin
assume x == y; /* [|-x+y>=0; x-y>=0|] /
x = x + 1; / [|-x+y+1>=0; x-y-1>=0|] /
y = y + 1; / [|-x+y>=0; x-y>=0|] /
x = x + 1; / [|-x+y+1>=0; x-y-1>=0|] /
y = y + 1; / [|-x+y>=0; x-y>=0|] */
end

But, ACDL when run with --octagons returns the following meet irreducibles after first deduction stage:
$guard#20
$guard#0
$cond#19

What is the reason for not deducing meet irreducibles similar to Interproc in the first deduction stage ?

For some real programs (derived from hardware designs), the chaotic iteration strategy seems to be very expensive. In particular, for a program of approx 200 LOC with multiple functions, a large portion of time is spent in the first deduction step (Decision Level 0). We need to implement other
iteration strategies for comparison:
1> Forward analysis with strongest post-condition -- over approximate analysis
2> Backward analysis with weakest pre-condition -- under approximate analysis

Let us consider the code below

int main(void) {
  int i=0;
  int x=0;
  x=5;
  while(i<1000) {
    i++;
    x--;
    assert(x>=5);
    assert(x<=5);
    assert(x>=0);
    assert(x<=0);
  }
 return 0;
}

If I run 2ls main.c, results are like

[main.assertion.1] assertion x >= 5: FAILURE
[main.assertion.2] assertion x <= 5: OK
[main.assertion.3] assertion x >= 0: OK
[main.assertion.4] assertion x <= 0: OK

Which part of the 2ls is likely to be responsible for this bug?

Find and delete the following statement during ACDCL run:
<refinement-iteration>1</refinement-iteration>

Works for intervals. We can avoid this check when we encounter octagonal constraints (two-variable meet irreducible). For example, consider the following scenario.
val = {x+y<=5, y+z<=10, ...}, m_ir = x+z<=3, then is_subsumed(m_ir, val)=true
The current is_subsumed check implementation cannot infer true for the above scenario. This may be due to the fact that the val is not guaranteed to be closed always. Or the logic of checking (!m_ir && val) is SAT does not work for two-variable meet irreducible.

Consider the program below:
{ int x, y; _Bool c; __CPROVER_assume(1 <= x && x <= 3); if(c) x++; else x--; assert(x<0); }
The SSA representation corresponding to the assignment of x#phi26 is wrong.

$cond#21 == (x#16 >= 1 && !(x#16 >= 4))
$cond#22 == (c#20 == TRUE)
$guard#22 == ($cond#21 && $guard#0)
x#23 == 1 + x#16
$guard#23 == (!$cond#22 && $guard#22)
$cond#24 == TRUE
x#25 == -1 + x#16
$guard#25 == ($cond#22 && $guard#22)
x#phi26 == ($guard#25 ? x#25 : x#23) // should this be x#phi26 == ($guard#25 ? x#23 : x#25)
$guard#26 == ($cond#24 && $guard#23 || $guard#25)
!(x#phi26 >= 0) || !$guard#26

Assignments below are missing from the SSA. The read-only variables (x#16, y#18) used for decision making are computed from these assignments.
x#16 == nondet_symbol(ssa::nondet16.1)
y#18 == nondet_symbol(ssa::nondet18.1)

Strategy to collect branch variables inside the preprocess routine so that decision heuristic don't need to compute these variables every time a decision is made. Pass these variables from acdl_solver to the decision heuristic.

With assumptions in the program, the decision heuristic can exploit the assumption statement to generate decisions on relevant variables such that the assumption constraint holds true.
For example, assume(x+y>4), the decisions can be x>=2 and y>=3.

This is irrespective of the fact that the octagonal constraints in the trail may not be able to derive the lower and upper bound of variable x and y, in which case a normal (less aggressive) decision heuristic would not be able to perform accurate splitting and hence can not take advantage of the assumption as shown above.

Consider a simple program below:
int main() {
int x=0,i;
for(i=0;i<=1;i++) {
x = x+i;
assert(x<1);
}
}
When I run 2ls on the above program, it shows VERIFICATION FAILED which is correct !!

Now, I just remove the braces around for loop and put the assertion outside the for loop.
int main() {
int x=0,i;
for(i=0;i<=1;i++)
x = x+i;
assert(x<1);
}

On executing the above program, 2ls shows VERIFICATION INCONCLUSIVE.
Shouldn't it terminate with VERIFICATION FAILED ?

Consider the program (regression: complete-check3) below.
int x, y; _Bool c; __CPROVER_assume(1 <= x && x <= 3); if(c) x++; else x--; assert(x<0); }
The SSA representation is below.

$cond#21 == (x#16 >= 1 && !(x#16 >= 4))
$cond#22 == (c#20 == FALSE)
$guard#22 == ($cond#21 && $guard#0)
x#23 == 1 + x#16
$guard#23 == (!$cond#22 && $guard#22)
$cond#24 == TRUE
x#25 == -1 + x#16
$guard#25 == ($cond#22 && $guard#22)
x#phi26 == ($guard#25 ? x#25 : x#23)
$guard#26 == ($cond#24 && $guard#23 || $guard#25)
!(x#phi26 >= 0) || !$guard#26

ACDL makes 4 decisions as shown below.
!cond#21, !cond#22, x#23 <= 2, x#25<=1

However, a single decision on !cond#22 should be sufficient to infer that the program is unsafe. Following optimizations are needed for this.

• Decisions on cond#21(assumption) is not necessary.
• Avoid decision on variables (x#23) assigned in infeasible path. This would require path-sensitive analysis. This means that x#23 should not be evaluated (ignored) when $guard#25 is TRUE.
• Furthermore, we just make a decision on the interval of x#25 = [0,2] to show that the program is unsafe.

When a structure is passed as an argument to a function, acdl shows the following error
identifier tag-state_elements_cell not found
Regression "TreeArb" in hw-acdlp shows the error.

Consider the program below:
!(x#22 == y#23 || !$guard#20)
TRUE
$guard#0 == TRUE
$guard#20 == ($cond#19 && $guard#0)
x#22 == 1u + x#20
y#23 == 1u + y#21
$cond#19 == (x#16 == y#18)
x#20 == 1u + x#16
y#21 == 1u + y#18

ACDL performed the following run:
DL0: propagate(AI) --> UNKNOWN
DL1: decide
Propagate(AI) --> UNKNOWN
DL2: decide
Propagate(AI) --> UNKNOWN
DL3: decide
Propagate(AI) --> BOTTOM
Learn: (!DL1 || !DL2 || !DL3), where DL3 is the last uip
Backtrack to DL2
Learned clause is UNIT, Propagation(PROPOSITIONAL) --> !DL2
Propagate(AI)
BOTTOM
Learn: (!DL1)
Backtrack to DL0, because the learnt clause has only one literal at present decision level
Propagate(PROPOSITIONAL) --> both learned clauses are Satisfying, no new propagation
Propagate(AI)
UNKNOWN
DL4: decide
Propagate(PROPOSITIONAL)
Propagate(AI)
.............
DL39:decide ...

This now continues with other decisions.
The point here is that when we propagated after the second backtrack, it lead to UNKNOWN.
That deviated the search. If this propagation had lead to BOTTOM, we would have terminated with
SAFE because we were already in DL0 and no further propagation would have been possible.

I identified that the problem is due to bad decision. And ACDL could not recover from bad decision in this example. The decisions are as follows:
DL1: (x#20 <= 1u)
DL2: (y#21 <= 1u)
DL3: (y#18 <= 1u)
Clearly, DL1 and DL2 are decisions on variables which are overwritten in SSA whereas DL3 is the decision on input variable which does not appear in the lhs of any SSA. If DL3 was made as the first decision, then ACDL would have terminated right after first backtracking since it would have identified the conflict in DL1 and immediately backtracked to DL0 to prove the remaining case safe.

A new decision added to the trail can lead to inconsistent trail (Abstract value is UNSAT).
Consider the following decision in octagon domain:
NEW DECISION:
(unsigned __CPROVER_bitvector[33])x#16 + (unsigned __CPROVER_bitvector[33])x#22 <= 1

Checking consistency of trail after adding decision:

$guard#20 && $guard#0 && $cond#19 && (signed __CPROVER_bitvector[33])x#16 - (signed __CPROVER_bitvector[33])y#23 <= 4294967294 && y#21 <= 1u && !(y#23 >= 3u) && !(-((signed __CPROVER_bitvector[33])y#23) >= 0) && !((unsigned __CPROVER_bitvector[33])x#22 + (unsigned __CPROVER_bitvector[33])y#18 <= 1) && (unsigned __CPROVER_bitvector[33])x#20 + (unsigned __CPROVER_bitvector[33])y#21 <= 1 && !(x#22 >= 3u) && !(-((signed __CPROVER_bitvector[33])x#22) >= 0) && !((unsigned __CPROVER_bitvector[33])x#20 + (unsigned __CPROVER_bitvector[33])x#22 <= 1) && !((unsigned __CPROVER_bitvector[33])x#20 + (unsigned __CPROVER_bitvector[33])y#21 <= 0) && !((unsigned __CPROVER_bitvector[33])x#22 + (unsigned __CPROVER_bitvector[33])y#21 <= 1) && !((unsigned __CPROVER_bitvector[33])y#18 + (unsigned __CPROVER_bitvector[33])y#21 <= 1) && !(-((signed __CPROVER_bitvector[33])x#16) >= 0) && (unsigned __CPROVER_bitvector[33])x#16 + (unsigned __CPROVER_bitvector[33])x#22 <= 1

The trail is inconsistent after addition of the last decision. This is because x#16>0 and x#22>0, so the last decision (x#16+x#22<=1) leads to UNSAT, thus making the trail inconsistent.

Presently, the consistency check happens inside the acdl solver when a decision heuristics returns a decision. But should it be part of the decision heuristics to abandon such decisions when it leads to inconsistent trail ?

Consider a program below:
int main() {
int x=0,i;
for(i=0;i<=6;i++) {
x = x+i;
assert(x<=10);
}
}

This leads to conjunction of 8 assertion statements for an unwinding of 7. A conjunction of all 8 assertions are passed to the ACDL solver. The SSA constraints generated for the following two commands are different:
1> 2ls --verbosity 10 --unwind 7
2> 2ls --acdl --decision D --propagate P --learning L --unwind 7

This leads to buggy verification output in ACDL.

Hi Peter,

What version of CProver/CBMC is this intended to be used with now-a-days?

All the best,

Dan.

An additional cond and guard variables are generated in the SSA. This was not in earlier SSA representation !! For example, consider the following program.
int main() { unsigned x,y,z; __CPROVER_assume(x+y>4); z=x+4; y=(x+z)/2; assert(y+z<=10); }

The corresponding SSA is as follows:

$cond#18 == x#15 + y#16 >= 5u
z#19 == 4u + x#15
$guard#19 == ($cond#18 && $guard#0)
y#20 == (x#15 + z#19) / 2u
!(y#20 + z#19 >= 11u) || !$guard#19
$cond#22 == !(y#20 + z#19 >= 11u)
$guard#23 == ($cond#22 && $guard#19)

Why do we need the variable cond#22 and guard#23 here ? This was not present in earlier SSA representation. This creates additional decision making for ACDL. Is there any way we can avoid this ?

Identification of read-only variables in SSA would assist concrete decisions in the gamma-complete phase. The following example demonstrate this.
Consider the program (regression: complete-check3) below.
int x, y; _Bool c; __CPROVER_assume(1 <= x && x <= 3); if(c) x++; else x--; assert(x<0); }
The SSA representation is below.
$cond#21 == (x#16 >= 1 && !(x#16 >= 4))
$cond#22 == (c#20 == FALSE)
$guard#22 == ($cond#21 && $guard#0)
x#23 == 1 + x#16
$guard#23 == (!$cond#22 && $guard#22)
$cond#24 == TRUE
x#25 == -1 + x#16
$guard#25 == ($cond#22 && $guard#22)
x#phi26 == ($guard#25 ? x#25 : x#23)
$guard#26 == ($cond#24 && $guard#23 || $guard#25)
!(x#phi26 >= 0) || !$guard#26

When a decision on !cond#22 is made, the potential gamma-complete variables are x#16, x#23. And the "don't care" variable which has no effect on assertion for the decision !cond#22 is x#25. The decision in gamma-complete check makes concrete decisions on x#16==2, x#23==3, but we need
just one decision in this case, which is x#16==2, since x#23 is derived from it. Here, x#16 is a read-only variable. So, a decision on x#16 is sufficient in this case.

For the following sv-comp benchmark (bitvector/jain_1_true-unreach-call.c ) with unwind 1, the SSA pre-processor did not terminate within 5 minutes.

extern void VERIFIER_error() __attribute ((noreturn));
extern int __VERIFIER_nondet_int(void);
void __VERIFIER_assert(int cond) {
if (!(cond)) {
ERROR: __VERIFIER_error();
}
return;
}
int main()
{
int y;
y = 1;
while(1)
{
y = y +2*__VERIFIER_nondet_int();
__VERIFIER_assert (y!=0);
}
return 0;
}

Consider a scenario where ACDL solver computed singletons for all variables (after several decisions and deductions). This means that there are no non-singletons left and hence no more decisions can be made. The gamma-completeness check can still fail for guard variables where it may find that the negation of a guard variable when conjuncted with the abstract value is not UNSAT (hence failed). But, this check is hurting us now.
Consider a guard variable in the assert statement.
(A) !(z#38 == -2 || !$guard#27)
ACDL deduced singletons for all variables in the program (guard#27=true, z#38=1, ... )
The gamma-completeness check passes for all variables in this program except guard#27.
However, guard#27 must be true for checking this assertion.
Does it make sense for gamma completeness check to fail for guard variable present in the assertion when we have already reached a concrete counterexample. Note also that the decision heuristics cannot make any further decisions since all variables are already singletons and there is no backtracking possible to make something non-singleton in this case.

Strategy to dynamically change the variable phase inside the decision heuristics.
This is relevant in the context of tpolyhedra heuristic ENABLE_HEURISTIC which biases the variable value to one extreme instead of a binary search. Such bias may be disadvantageous for some program. For example, learning0 regression suffers because of this heuristic.

The closure check for deductions does not work correctly with the following domain operation.
domain(true_exprt(), all_vars, old_val, new_val, deductions)
Here statement = true_exprt and all_vars contains all variables in the program, which is the sub-domain. So, we want to find all transitive dependencies when domain=subdomain. The problem may be due to following two cases:
1> Incorrect creation of sub-domain
2> when true_exprt() is popped, there is no variable in the statement to project on.

Adding command line flags in 2ls for different iteration strategies supported by acdl.
--deduce N where N = {forward, backward, chaotic}

ACDL now checks one assertion at a time. We need to add support for checking multiple assertions simultaneously.

Consider the program below:
int main() {
int x=0,i;
for(i=0;i<=1;i++)
x = x+i;
assert(x>25);
}

The SSA after unwinding=2 is shown below:
!(x#phi21 >= 26 || !$guard#25)
!$guard#ls24%2
x#17 == 0
$cond#24%2 == TRUE
$guard#0 == TRUE
$cond#24%1 == TRUE
i#20 == 0
$guard#25 == ($cond#21 && $guard#21)
x#phi21 == x#phi21%0
x#phi21 == ($guard#21%2 && $cond#21%2 ? x#phi21%2 : ($guard#21%1 && $cond#21%1 ? x#phi21%1 : x#phi21%0))
$cond#21 == $cond#21%0
$guard#21 == $guard#21%0
$cond#21 == ($guard#21%2 && $cond#21%2 ? $cond#21%2 : ($guard#21%1 && $cond#21%1 ? $cond#21%1 : $cond#21%0))
$guard#21 == ($guard#21%2 && $cond#21%2 ? $guard#21%2 : ($guard#21%1 && $cond#21%1 ? $guard#21%1 : $guard#21%0))
x#22%0 == i#phi21%0 + x#phi21%0
x#phi21%0 == ($guard#ls24%0 ? x#lb24%0 : x#17)
x#phi21%0 == x#22%1
x#22%1 == i#phi21%1 + x#phi21%1
$guard#22%1 == (!$cond#21%1 && $guard#21%1)
x#22%2 == i#phi21%2 + x#phi21%2
$guard#22%2 == (!$cond#21%2 && $guard#21%2)
x#phi21%1 == x#22%2
$cond#21%1 == i#phi21%1 >= 2
$guard#21%1 == ($guard#22%2 && $cond#24%2)
x#phi21%2 == ($guard#ls24%2 ? x#lb24%2 : x#17)
$cond#21%2 == i#phi21%2 >= 2
$guard#21%2 == $guard#0
i#phi21 == ($guard#21%2 && $cond#21%2 ? i#phi21%2 : ($guard#21%1 && $cond#21%1 ? i#phi21%1 : i#phi21%0))
$guard#22%0 == (!$cond#21%0 && $guard#21%0)
$cond#21%0 == i#phi21%0 >= 2
$guard#21%0 == $guard#0
$guard#21%0 == ($guard#22%1 && $cond#24%1)
i#23%0 == 1 + i#phi21%0
i#phi21%0 == ($guard#ls24%0 ? i#lb24%0 : i#20)
i#phi21 == i#phi21%0
i#phi21%0 == i#23%1
i#23%1 == 1 + i#phi21%1
i#phi21%1 == i#23%2
i#23%2 == 1 + i#phi21%2
i#phi21%2 == ($guard#ls24%2 ? i#lb24%2 : i#20)

IMPLICATION GRAPH AFTER DEDUCTION PHASE

!(i#phi21 >= 3)
!(i#lb24%0 >= 3)
!(-((signed __CPROVER_bitvector[33])i#23%0) >= -2)
!(i#23%0 >= 4)
!(-((signed __CPROVER_bitvector[33])x#phi21) >= 0)
!(x#phi21 >= 2)
!(-((signed __CPROVER_bitvector[33])x#lb24%0) >= 0)
!(x#lb24%0 >= 2)
!(-((signed __CPROVER_bitvector[33])x#22%0) >= -2)
!(x#22%0 >= 4)
!(i#phi21%0 >= 3)
!(-((signed __CPROVER_bitvector[33])x#phi21%0) >= 0)
!(x#phi21%0 >= 2)
!(i#23%1 >= 3)
!(-((signed __CPROVER_bitvector[33])x#22%1) >= 0)
!(x#22%1 >= 2)
$guard#22%2
!(-((signed __CPROVER_bitvector[33])x#phi21%1) >= 1)
!(x#phi21%1 >= 1)
!(i#23%2 >= 2)
!(i#phi21%1 >= 2)
!(x#lb24%0 >= 26)
$guard#21%1
!$cond#21%1
!$cond#21%2
!(-((signed __CPROVER_bitvector[33])x#22%2) >= 1)
!(x#22%2 >= 1)
!(i#phi21%2 >= 1)
!(-((signed __CPROVER_bitvector[33])i#phi21%2) >= 1)
!(i#phi21%2 >= 2147483646)
!(-((signed __CPROVER_bitvector[33])i#23%2) >= 0)
!(i#23%2 >= 2147483647)
!(-((signed __CPROVER_bitvector[33])i#phi21%1) >= 0)
!(i#phi21%1 >= 2147483647)
!(-((signed __CPROVER_bitvector[33])i#23%1) >= -1)
!(-((signed __CPROVER_bitvector[33])i#phi21) >= -1)
!(-((signed __CPROVER_bitvector[33])i#lb24%0) >= -1)
$guard#ls24%0
$guard#22%1
!(-((signed __CPROVER_bitvector[33])i#phi21%0) >= -1)
!$guard#22%0
$guard#21%2
!(-((signed __CPROVER_bitvector[33])x#phi21%2) >= 1)
!(x#phi21%2 >= 1)
!(x#22%1 >= 26)
$guard#21%0
$cond#21%0
!(x#phi21%0 >= 26)
$guard#21
$cond#21
!(-((signed __CPROVER_bitvector[33])i#20) >= 1)
!(i#20 >= 1)
$cond#24%1
$guard#0
$cond#24%2
!(-((signed __CPROVER_bitvector[33])x#17) >= 1)
!(x#17 >= 1)
!$guard#ls24%2
!(x#phi21 >= 26)
$guard#25

Completeness check

The value i#lb24%2
is not complete

The variable i#lb24%2 is expected to be deduced, but it is not deduced -- hence the bug is in deduction. However, the variable i#lb24%0 is correctly deduced. ACDL should return with successful gamma-completeness check in this case.

We get the following error for decisions made in octagon analysis.
acdl_solver.cpp:563: bool acdl_solvert::decide(const local_SSAt&, const exprt&): Assertion `domain.check_val_consistency(new_value)' failed.

An example program to reproduce the error is shown below:
unsigned x,y,z; __CPROVER_assume(x+y>4); z=x+4; y=(x+z)/2; assert(y+z<=10);

This need to be run with the following settings:
--acdl --acdl-decision octagon --acdl-conflict first-uip --octagons --verbosity 10

Check for regression: completeness-check2
The number of templates returned now is zero.

Below, I demonstrate an example to show that the propositional level UIP computation can not be lifted to relational domain, like octagons. This also means that unit-ness guarantee for learnt clause (after backtracking) in octagon domain is not straight-forward.
Abstract value (A): (x+y > 0 && x-y < 2 && y-z <= 0 && z-y <= 0),
where (x+y > 0 && x-y < 2 ==> x=y+1) and (y-z <= 0 && z-y <= 0 ==> y==z)

Learnt clause: (L1 || L2 || L3) = (x > 10 || z > 3 || y+z < 5), obtained by negating
decisions {D1, D2, D3} as (L1 = !D1, L2 = !D2, L3 = !D3)

Let us check whether the learnt clause is UNIT wrt. abstract value above.

Checking L1 wrt. A : (x>10) wrt. (x+y > 0 && x-y < 2 && y-z <= 0 && z-y <= 0),
L1 is UNKNOWN as no information can be derived from a single literal 'x' in L1

Checking L2 wrt. A : (z>3) wrt. (x+y > 0 && x-y < 2 && y-z <= 0 && z-y <= 0),
L2 is UNKNOWN as no information can be derived from a single literal 'z' in L2

Checking L3 wrt. A : (y+z<5) wrt. (x+y > 0 && x-y < 2 && y-z <= 0 && z-y <= 0),
L3 is CONTRADICTING with y-z <= 0 && z-y <= 0

Hence, the learnt clause is not UNIT. Unit-ness of a clause requires all literals of a clause to be CONTRADICTING but one. The non-contradicting literal must be UNKNOWN and not SATISFIABLE.

An important point to note here for the above unit-ness check is that the literals participating in a learnt clause are also dependant on each other. As soon as literals denote relation between first-order variables, the pure reasoning on boolean skeleton is not sufficient.

Checking L1:
(x>10) ==> y>9
(y>9) ==> !(y+z < 5), which violates L3 since z>3

An alternative is to simply pass the learnt clause to domain to make deductions, but domain may simply deduce the following UNKNOWN literals:
(x > 10, z > 3)

Handle the following case in domain normalization: (x==5 && x<=10)
The equality (x==5) comes from the new concrete decision heuristic introduced by the gamma-complete check phase. So, the domain normalization operator should handle such case.

Domain Subsumption checks are very expensive operations (obtained from MiniSAT statistics). So, we need an alternative cheaper syntactic subsumption check in ACDL.

The regression branch7 computes the learnt clause with the first-UIP which is not UNIT.
Learnt clause: !(-((signed __CPROVER_bitvector[33])id#return_value#32) >= -1) || !(!(a#31 >= 0))
Comparing relevant expressions !(a#31 >= 3) && !(-((signed __CPROVER_bitvector[33])a#31) >= 2) <---> !(!(a#31 >= 0))
The status is 1
2ls: acdl_analyze_conflict_base.cpp:195: bool acdl_analyze_conflict_baset::operator()(const local_SSAt&, acdl_conflict_grapht&): Assertion `result==3' failed.

Simply, this is checking the value (a>-2 && a<3) with the meet irreducible in the learnt clause which is a>=0. Clearly, this is UNIT.

Consider the following SSA statement:
cond=(x==y)OR(x==-y)
Making decision like cond=1 always makes the rhs true. However, an effective decision would be to
make individual decisions on x==y and x==-y.
Such decisions can be made by first identifying disjunctions in rhs of cond statements. If there is such a disjunction, then assign each component of disjunction to a new expression. For example cond1=(x==y), cond2=(x==-y). The assignment to new expression should take place in pre-processing step. Then insert cond1 and cond2 to decision variables vector and pass them to respective decision heuristics implementation.

Make separate class for different initialisation of conflict reasons. Currently, we have two heuristics -- 1) pure decision-based and 2) decision+trail elements at deepest decision level that contradict with the final transformer

Consider the following trail where x,y,z are unsigned integers.
{x>=0, z<=5, x+y <= 10, y+z <=8}

How can we determine the lower bound and upper bound for x,y,z ?
x = [0,?], y=[?,?], z=[0,5];
Manually, this can be computed as x = [0,7], y=[0,3], z=[0,5];

Consider the SSA below :
!(return_value_f$1#27 == return_value_g$2#39 || !$guard#0)
$guard#0 == TRUE
return_value_f$1#27 == f#return_value#24
return_value_g$2#39 == g#return_value#36
f#return_value#24 == x#23
g#return_value#36 == x#35
x#23 == 1u + x#22
x#35 == 1u + x#34
x#22 == x#16
x#34 == x#16

It should be optimised to the following with pre-processing:
!(x#23 == x#35 || !$guard#0)
$guard#0 == TRUE
x#23 == 1u + x#16
x#35 == 1u + x#16

Cache sum and difference constraints over symbols so that we do not have to regenerate templates over same variables every time numerical inference is called.

Consider the program below:
{ int x, y; _Bool c; __CPROVER_assume(1 <= x && x <= 3); if(c) x++; else x--; assert(x<0); }
The assumption is represented in SSA as follows.
$cond#21 == (x#16 >= 1 && !(x#16 >= 4))

Currently, ACDL makes decision on cond#21. But a decision on cond#21 is not necessary since it must always hold TRUE.

Consider the program below
int main() { unsigned x, y; _Bool op; __CPROVER_assume(x==y); if(op) x++; else x--; if(op)
y=y+1; else y=y-1; assert(x==y); }

The Fall Back strategy performs first few (~50) iterations using ACDLP solver. If the problem can not be solved in 50 iterations, then it invokes the SAT solver with the conjunction of SSA and the trail element computed by ACDLP so far (current abstract value). Experiments suggest that the abstract value computed by ACDLP so far indeed helps SAT Solver to solve the problem much more efficiently.

Few Statistics that support this observation for the example above:

SAT solver statistics without ACDLP (Problem solved solely by Propositional SAT Solver)

restarts : 4
conflicts : 423
decisions : 2516
propagations : 38617
conflict literals : 2905

SAT solver statistics with ACDLP (Initial iterations performed by ACDLP followed by Propositional SAT Solver)

restarts : 0
conflicts : 0
decisions : 0
propagations : 173
conflict literals : 0

from https://github.com/diffblue/cbmc/tree/goto-analyzer-develop/src/analyses/variable-sensitivity

The algorithm below for forward iteration strategy over SSA has limitations :
Step 1: Populate worklist with leaves (rhs doesn't have any dependencies)
Step 2: Propagate/deduce right to left (pass lhs variable of the statement to acdl_domain())
Step 3: Add to the worklist the nodes of which all predecessors have been processed.

Now, consider SSA representation for a program:
N1: !(x#20 == 1u + y#18 || !$guard#20)
N2: $guard#0 == TRUE
N3: $cond#19 == (x#16 == y#18)
N4: x#20 == 1u + x#16
N5: $guard#20 == ($cond#19 && $guard#0)

The leaf nodes are : N2, N3, N4
When N3 is popped, we cannot deduce any information since deductions in N3 depends on deductions in N5 (cond#19). In other words, the deductions in leaf nodes depends on deductions in non-leaf nodes. So, following Step 3 of above algorithm, the deductions in node N3 that (x#16 == y#18) is never possible since (cond#19) is not known when N3 is processed and is only known when N5 is processed.

Split operation must handle constraints like x==N in addition to x<=N and x>=M. When x==N, the lb = N and ub=N, so x==N must be returned.

In presence of the constraint x==N in the trail, can the octagonal analysis interpret this correctly ?

Deductions using octagon domain are too restricted now. So, we miss some valid deductions despite legitimate projections on live variables.
NOTE: We have to consider all template rows that contain at least one live variable (not only those rows that contain only live variables).

Consider the following scenario:
Value:
1<=x'-x
x'-x<=1
0<=x-y
x-y<=0

Pop: x'=x+1
Deductions: (project on x', x, y)
1<=x'-y <== 0<=x-y
x'-y<=1 <== x-y<=0
Value:
1<=x'-x
x'-x<=1
0<=x-y
x-y<=0
1<=x'-y
x'-y<=1

For the above example, the deductions in bold (over x' and y) are missing.

Current subsumption check using SAT call solver << and_exprt(conjunction(value), not_exprt(m)) may subsume valid meet irreducibles in presence of octagonal constraints, which may further block the propagation phase from deducing closed abstract value.
We change the subsumption check to the following. Assume the function is_subsumption(A,m) where we want to determine if m is subsumed by abstract value A.
Step 1: Normalize all expressions in A as well as m (that is, !(x<=10) to (x>10))
Step 2: Collect all lhs templates of the meet irreducibles in A that matches with lhs of m in a vector value.
Step 3: Check using solver whether and_exprt(conjunction(value), not_exprt(m)) is SAT or UNSAT. If SAT, then m is not subsumed by A, else m is subsumed by A.

Following scenario shows invalid result produced by the abductive generalisation transformer:
Input::
Initial value:: $guard#25 && !(x#phi25 >= 1) && !(-((signed __CPROVER_bitvector[33])x#phi25) >= 1) && $cond#23 && $guard#0 && !$cond#21 && !$guard#24 && $guard#22 && !(-((signed __CPROVER_bitvector[33])x#16) >= 1)

Antecedent clause (statement):: x#phi25 == ($guard#24 ? x#24 : x#22)

Final value:: !(x#22 >= 1) && !(-((signed __CPROVER_bitvector[33])x#22) >= 1)

Variable set:: $cond#21 $cond#23 $guard#0 $guard#22 $guard#24 $guard#25 x#16 x#22 x#24 x#phi25

Output:
Generalization of Initial value:: !(x#22 >= 1) && !(-((signed __CPROVER_bitvector[33])x#22) >= 1)

We want a generalisation of the initial value. But the adductive transformer simply returns the same final value that is passed to the following abductive transformer.
ssa_analyzer(*solver, SSA, implies_exprt(conjunction(final_value), statement), template_generator);

K-induction proof seems to be buggy in 2ls. The following benchmark reproduce the bug.
https://github.com/rajdeep87/verilog-c/tree/master/safe/hwmcc15/6s177

@peterschrammel The proof fails showing "k-induction counterexample found after 0 unwinding(s)". However, CBMC proves it safe for 100 unwindings. Also, the benchmark is SAFE for more than 100 unwindings.
Command line option used : --k-induction --inline --havoc --competition mode

Handling the SSA enabling expression for loops..
Given the enabling expression for SSA as (!enable0 && enable1), we must not pass SSA nodes that corresponds to enable0 to the worklist and should only pass SSA nodes corresponding to enable1 to the worklist.

Consider the structure in regression "FIFO":
struct state_elements_rbFIFO{
_Bool empty;
unsigned char mem[16];
unsigned char head;
unsigned char tail;
};
struct state_elements_rbFIFO srbFIFO;

ACDL cannot split decision variable srbFIFO.mem because its type is unsigned char (warning below).
WARNING: do not know how to split srbFIFO.mem#166 of type unsigned char [16l]

Need to support splitting for unsigned char.