Non-deterministic assertion error at src/btorslvquant.c:1054

[rainoftime]

Hi, for the following formula, boolector 6fce0ac

(set-logic BV)
(declare-fun _substvar_16_ () Bool)
(declare-fun _substvar_17_ () Bool)
(declare-const v0 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v11 Bool)
(declare-const v13 Bool)
(assert (forall ((q0 (_ BitVec 1)) (q1 Bool)) (not (and v0 q1 q1 v11 q1 q1 q1 true q1 q1 v7))))
(assert (or _substvar_17_ _substvar_16_))
(declare-const v15 Bool)
(declare-const v24 Bool)
(check-sat)

$ seq 20 | xargs -Iz ./boolector --engine fun --quant-synth elmr xx.smt2                                                           
sat
sat
sat
sat
sat
sat
sat
sat
[btorslvquant] refine_exists_solver: invalid refinement '-1 bvconst 0'
sat
sat
sat
sat
sat
sat
[btorslvquant] refine_exists_solver: invalid refinement '-1 bvconst 0'

[aytey]

Just to speed things along: how did you configure Boolector? What SAT solvers did you enable?

Why am I asking? Well, this could be an uninitialised read inside of the Boolector code, or it could be an an uninitialised read inside one of Boolector's dependancies.

For me, with a build that only uses Lingeling, I cannot reproduce this issue.

[rainoftime]

I re-build boolector with lingeling (there is only lingeling in boolector\dep

./configure.sh -g --asan

-- Found PythonInterp: /usr/bin/python (found version "2.7.12") 
-- Build type: Debug
-- Shared build: yes
-- ASAN support: yes
-- UBSAN support: no
-- Assertions enabled: no
-- gcov support: no
-- gprof support: no
-- Logging support: yes
-- Python bindings: no
-- Time statistics: yes
-- CaDiCaL: yes
-- CryptoMiniSat: yes
-- Lingeling: yes
-- MiniSat: yes
-- PicoSAT: yes
-- GMP: no

The error info seems different

boolector: /boolector/src/btorslvquant.c:1054: refine_exists_solver: Assertion `res != e_solver->true_exp' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
xargs: /boolector: terminated by signal 6

[rainoftime]

(set-logic BV)
(declare-fun _substvar_111_ () Bool)
(declare-const v2 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const bv_2-1 (_ BitVec 2))
(declare-const v39 Bool)
(assert (not (exists ((q0 Bool)) (or (not (or q0 q0 v6 v2 q0 q0 q0)) _substvar_111_ v5))))
(check-sat)

[mpreiner]

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.