Basile Clément
Basile Clément
> @bclement-ocp Thank you for your comments. Concerning the benchmark, you should read the leftmost column `x.xxxu`, as it shows the user time. The next column shows the system time,...
@Stevendeo looks like this is solved by #520, should we close?
This no longer reproduces after e357e6a828124ed2553ec901728edf381862a77f so it looks like #487 fixed it.
Closing as the GUI has been removed in #601
Models are on stdout as per smtlib recommendations; the second issue is fixed. Closing. We should consider printing the models from `--dump-models` on stderr (or have a configuration flag for...
There are two compounding bugs here: - First, in `check_records`, we assume that any function that returns a record is a record constructor (and any function of one argument taking...
Looks like this is AC(X) exploding by trying to saturate way too many equations involving `f(x)`, `f(x + 1)` and variants. Either inlining `f` or abstracting it (making it uninterpreted)...
SMT-LIB version: ```smt-lib (set-logic ALL) (declare-const ui_0 Int) (assert (exists ((ieqv0 Int)) (forall ((iuqv0 Int)) (= (* ieqv0 ieqv0) iuqv0)))) (assert (forall ((iuqv0 Int)) (>= ui_0 iuqv0))) (check-sat) ``` Interestingly...
It looks like the runaway loop is due to wrong pattern inference on the first quantifier when under the existential: in the manually skolemized version, the trigger is `iuqv0`, while...
It looks like the issue is indeed related to the "triggers of the existential" thing. We do multiple rounds of instantiation. In the first round (where we don't allow inferring...