Description
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