diff options
| author | Ying Sheng <sqy1415@gmail.com> | 2019-12-16 11:42:36 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-16 11:42:36 -0800 |
| commit | 49f0f09c6ef1c04fcd5b088456cea9998cff3c91 (patch) | |
| tree | 0d5746c90c1e7ca3e336a8cfc7417b05c0eecbe8 /test/unit | |
| parent | c101a6b42d1f14bc750fb2328ddd83261148d7ae (diff) | |
Support ackermannization on uninterpreted sorts in BV (#3372)
Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/theory/theory_bv_white.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index bc5f73435..5af01c0cf 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -68,6 +68,8 @@ public: } void testBitblasterCore() { + d_smt->setLogic("QF_BV"); + d_smt->setOption("bitblast", SExpr("eager")); d_smt->setOption("incremental", SExpr("false")); // Notice that this unit test uses the theory engine of a created SMT |