Alberto Gonzalez

Results 2 issues of Alberto Gonzalez

I typically call Yices in EF `BV` mode repeatedly, each time on a very slightly different problem--only one constant argument to a `bvule` changes. The idea is to assert some...

Background ---- [I noticed](https://github.com/SRI-CSL/yices2/issues/205#issuecomment-623030632) that, for one of my [example `BV` exists-forall problems](https://github.com/boqwxp/yosys-examples/blob/master/example1/example.smt2), `time` reported that yices spent a full third of its wall-clock time in the kernel. When I...