| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
The issues here are mostly with induction (wrt. to trigger selection and
quantifier splitting) and with expressions like P(i, j-1) where no good choices
are available.
|
| |
|
|
|
|
|
|
|
|
| |
class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
|
| | |
|
| |
|
|
| |
literals around if-then-else as a surprising source of practical hanging.
|
|
|
Generates 'computing' axioms for both all formals and just decreasing formals.
Supported are literal datatypes, booleans and numbers.
The axioms are given a weight of 10, which seems enough for Z3 to give up when
it is sane to do so.
|
Clément Pit--Claudel
leino
Nada Amin
Unknown