Mathias Preiner

The following `yices_push(ctx)` call produces the below error with a debug build commit 09f162107cc9140172e6c890d8ccc633126c3720. ``` #include "yices.h" int main() { yices_init(); type_t s1 = yices_real_type(); term_t t1 = yices_new_uninterpreted_term(s1); term_t...

JavaScript heap out of memory

7

I'm running into an out of memory problem in a larger C++ project (https://github.com/mpreiner/CVC4/runs/351674288). I checked the size of the lcov.info on my machine an it's 95M. The 2048M heap...

yinyang (version 0.3.0 installed via pip) consumes ~40G of memory when running with the provided `semantic-fusion-seeds/QF_SLIA` seeds. Using more seeds will increase memory consumption (with the QF_SLIA logic from SMT-LIB...

No warning when no quantifiers are used in quantified logic

4

It would be great if Dolmen warns if no quantifiers are used, but a quantified logic was specified: For example for ``` (set-logic BV) (declare-const a (_ BitVec 8)) (declare-const...