rainoftime

# Contributing to CSrankings Thanks for contributing to CSrankings! Here are some guidelines to getting your pull request accepted. 0. Use a reasonable title that explains what the PR corresponds...

yices f705557b7d33d866eb1 ~~~~ (set-logic ALL) (declare-fun B () (Array (Array Int Bool) (Array Int Bool))) (declare-fun C () (Array (Array (Array Int Bool) (Array Int Bool)) Bool)) (assert (C B))...

Assertion error at exists_forall/ef_values.c:745

1

950709adcb8e8ff26190 ~~~~ (set-logic UF) (declare-const x Bool) (declare-fun v () Bool) (declare-sort S 0) (assert (or v (and (not v) (forall ((q Bool)) (exists ((q S)) (forall ((q3 S)) (forall...

get-interpolant interface for SMT-LIB2 frontend

1

Hi, I observed the recent paper "Interpolation and Model Checking for Nonlinear Arithmetic". It seems that in the SMT-LIB2 frontend, Yices only exposes the `get-unsat-model-interpolant` interface. Will the interpolant generation...

QF_NRA models are approximate

2

Hi, for this formula, yices 7139142 givens an invalid model [invalid_nra.txt](https://github.com/SRI-CSL/yices2/files/5379016/invalid_nra.txt) When feeding the model to yices and cvc4, the solvers decide the formula is unsat. [invalid_nra_replace_by_model.txt](https://github.com/SRI-CSL/yices2/files/5379017/invalid_nra_replace_by_model.txt)

Performance issue on QF_NIA formula

1

Hi, for the following formula ~~~~ (set-logic QF_NIA) (declare-const i3 Int) (declare-const i19 Int) (assert (= 538 (* 136 (+ 56 354 0 0 (- i19 18 i3))))) (check-sat) ~~~~...

Assertion violation at symbolic.cc:106 (optimiation instance)

1

Hi, for the following formula ~~~~ (set-logic QF_NRA) (declare-const v0 Bool) (declare-const v1 Bool) (declare-const v2 Bool) (declare-const v17 Bool) (declare-const r2 Real) (declare-const r6 Real) (declare-const r7 Real) (declare-const...

std::runtime_error for optimization instance

1

Hi, for the following optimization instance, ~~~~ (set-logic QF_NRA) (declare-const v0 Bool) (declare-const v1 Bool) (declare-const v2 Bool) (declare-const v3 Bool) (declare-const v5 Bool) (declare-const v6 Bool) (declare-const v7 Bool)...

Hi, for the following formula ~~~~ (set-logic QF_NRA) (declare-const r2 Real) (declare-const r5 Real) (declare-const r6 Real) (assert (or (or (>= 6455254657.0 r6) (>= 6455254657.0 r6) (>= 6455254657.0 (- 6.0...

GPU or Xeon Phi support?

1

Is there any plan to add GPU or Xeon Phi support? Thanks in advance, Jack