Bruno Dutertre

Model interpolants should be displayed in the SMT syntax

2

Running `yices-smt2 --incremental` on `tests/regress/mcsat/nra/assumptions/quadratic.smt2` will produce this output: ``` unsat (or (>= (* -1 a) 0) (>= (+ (* -4 a c) (^ b 2)) 0)). unsat (or (>=...

Hi, We've just found a bug in your parser related to the get-value command. The SMT-LIB syntax for get-value is ``` (get-value ( + )) ``` (cf. SMT-LIB 2.6 page...

Not all instructions handle vector arguments

2

Need to fix Trunc, Zext, Sext, Bitcast?, Inttoptr, Ptrtoint, Select, and Getelementptr?. They are allowed to have vector operands and return vector values (all of the same length). The instructions...

make check on MacOS X

13

'make check' can be made to work on a Mac but it's hard. Several issues get in the way: - pip doesn't work with the default system python because of...