Age | Commit message (Collapse) | Author |
|
Fixes two issues in regressions, fixes regress1.
|
|
* Fixed bug 3662
* format
* small change
* added bug3663.smt2 file
* throw Logic Exception
* throw Logic Exception
* ;EXIT: 1
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(#3641)
|
|
|
|
|
|
apps (#3605)
|
|
|
|
|
|
|
|
* rewrote set cardinality for finite-types
* small changes and format
|
|
|
|
Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced.
This fixes #3587.
|
|
Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).
Also improves support in a few places for tolower/toupper.
|
|
transcendentals (#3577)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).
|
|
|
|
|
|
solver (#3525)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|