- May 04, 2021
-
-
Marek Chalupa authored
+ a few comments
-
Marek Chalupa authored
These may not be valid
-
- May 03, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Store just a sequence of sets and their union. In the future, we'll store also an incremental solver for fast queries about sequences.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
This reverts commit 4cb07686.
-
Marek Chalupa authored
Not only if we give up extending it or we prove it is safe. This way, we store all sequences that we ever create.
-
- Apr 30, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
- Apr 29, 2021
-
-
Marek Chalupa authored
This reverts commit 62d66147. That commit breaks things, we need to solve it better.
-
- Apr 28, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Do not keep those that are surely unreachable.
-
Marek Chalupa authored
Concrete bool has not rewrite_and_simplify() method.
-
Marek Chalupa authored
We must substract 1.
-
Marek Chalupa authored
A step to soundness again.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
And infer more of them.
-
Marek Chalupa authored
We can reduce only equalities atm...
-
- Apr 27, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
We cannot rewrite exprs with assuming exprs...
-
Marek Chalupa authored
This reverts commit 0d4254eb. This was wrong, it worked well.
-
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.
-