- Apr 27, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We didn't finish the lhs transformation before replacing the rest of the formula.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
There it can happen, that we do not match all inputs and we fail on assertions.
-
Marek Chalupa authored
If found that it holds in more consecutive states.
-
Marek Chalupa authored
This test was on the edge...
-
Marek Chalupa authored
Re-use the overapprox_state method that we already have.
-
Marek Chalupa authored
Do not generate relations for pre-prestates, just check whether the already generated relations for pre-state hold.
-
Marek Chalupa authored
Do not create a set if it is already a set.
-
Marek Chalupa authored
To filter out the relations that are not definitely useful.
-
Marek Chalupa authored
No functional changes.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
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
-