HomeIsabelle/Phabricator

added a bound in SMT on the number of schematic constants considered -- the…

Description

added a bound in SMT on the number of schematic constants considered -- the code (in for_schematics) is exponential in that number

Details

Provenance
blanchetteAuthored on
Parents
rISABELLE854e9223767f: tuned signature;
Branches
Unknown
Tags
Unknown