diff options
| author |  Rustan Leino <unknown> | 2014-06-10 18:15:59 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-06-10 18:15:59 -0700 |
| commit | 92991242c8ea361b8da5a83bd19462b216387618 (patch) | |
| tree | b4fc209784850986f05bfcdf7e80957e520ad819 /Test/vstte2012 | |
| parent | 2dcb445f1addae38aff40d5a153952ee7b4130e5 (diff) | |
Specialized Lit function for int and real (leaving all other cases polymorphic). This reduces the number of int<->U conversions that Boogie adds, which avoids a looping problem in Z3.
(Regrettably, the test suite seems to have become rather unstable. Sometimes everything verifies and sometimes there is some looping forever.)
Diffstat (limited to 'Test/vstte2012')
0 files changed, 0 insertions, 0 deletions