- Apr 23, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
If you match the set created from exit states to some inductive set, use the inductive set (all of them unified).
-
Marek Chalupa authored
Regression tests that I forgot to add.
-
Marek Chalupa authored
So that we can run tests until we support that.
-
Marek Chalupa authored
-
Marek Chalupa authored
We can compare also two pointers.
-
Marek Chalupa authored
-
Marek Chalupa authored
Mainly for BSE.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Do not over-write the containers that are iterated, etc.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We do not need to know anything like "unknown" or "uninit", since that is almost always the case.
-
Marek Chalupa authored
-
- Apr 22, 2021
-
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
Directly add memory constraints for init states.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
maybe_sat seems to be broken (see assume_regression test)
-
Marek Chalupa authored
(at least some)
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
In joining states, just assume that the state is feasible after some time of solving.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We do not know what to do else.
-
Marek Chalupa authored
The check was not called as it was in a wrong instance of method.
-
Marek Chalupa authored
Forgot to add this to git.
-
Marek Chalupa authored
Not in parser, the calls may be unreachable.
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
-
Marek Chalupa authored
We store 1b values into 1B values, which is not nice and must be taken care of.
-