- Apr 27, 2021
-
-
Marek Chalupa authored
-
- Apr 26, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We tried to ask whether constraints are sat given the assumption that they are sat.
-
Marek Chalupa authored
No functional change.
-
Marek Chalupa authored
This reverts commit 38d5a278. It breaks things. We must do that part by part and check for regressions.
-
Marek Chalupa authored
So that we do not choke there.
-
Marek Chalupa authored
This method computes the precondition for one loop iteration.
-
Marek Chalupa authored
Make them return self, so that we can chain them.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We cannot intersect them together, assumptions are always on their own (we could create unsat assumption if we intersect them -- since those created from path condition are speculative and may not hold together in the state).
-
Marek Chalupa authored
We want to simplify the formula as much as possible.
-
Marek Chalupa authored
-
Marek Chalupa authored
To match the rest of namings.
-
Marek Chalupa authored
-
- Apr 24, 2021
-
-
Marek Chalupa authored
It will be handy in the future.
-
Marek Chalupa authored
sequences That is, also when we hit the loop 2nd or more times.
-
Marek Chalupa authored
-
Marek Chalupa authored
This reverts commit 82fd5ac7. It breaks tests.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Relations should just help, not to choke the algorithm.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Add a thershold option for that.
-
Marek Chalupa authored
If we remove them, we it may happen that we will fail creating new sis -- reusing the sequences does not lead to recomputation. First, we union them together. Second, they are overapproximated w.r.t a different error set, so their extensions are different than before.
-
Marek Chalupa authored
-
Marek Chalupa authored
Do BSE until we actually unroll the loop maxk times.
-
Marek Chalupa authored
Allow printing also when not in debug mode.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Fix generate the expression whether the pointers may be equal and check whether it simplifies to false (which is mostly the case). If so, do not try to proceed further where we can fail on unsupported comparison of symbolic pointers and addresses.
-