- Apr 27, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
Not only when we have an assumption.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
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.
-