Assertion violation at src/btornode.c:1998

[rainoftime]

Hi, for the following formula, boolector 6fce0ac

(declare-const v1 Bool)
(declare-const v4 Bool)
(declare-const v8 Bool)
(declare-const v11 Bool)
(declare-const v14 Bool)
(assert (forall ((q111 (_ BitVec 4)) (q112 (_ BitVec 6)) (q113 (_ BitVec 7)) (q114 (_ BitVec 38))) (xor true true true true true (exists ((q17 (_ BitVec 6)) (q18 (_ BitVec 7)) (q19 (_ BitVec 7))) (distinct v8 v11 v1 (not (forall ((q0 Bool) (q1 Bool)) (not (or q1 q0)))) (distinct (exists ((q0 Bool) (q1 Bool)) (not (= (not (forall ((q0 Bool) (q1 Bool)) (not (or q1 q0)))) v4 q0 true v11))) v11) v14 v4)) true true)))
(check-sat)

$ boolector yy.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/btornode.c:1998: new_quantifier_exp_node: Assertion `!btor_node_param_is_bound (param)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted

[vedadux]

Here is a related example:

(declare-const v Bool)
(assert (forall ((q (_ BitVec 38))) 
    (distinct true 
        (exists ((p (_ BitVec 7))) 
        (distinct false v (distinct v 
            (exists ((w Bool)) w))))
    )))
(check-sat)

The verbose output I get is:

[btor>main] Boolector Version 3.2.2 master-0783aa844db69953a3271bf4957b54b80a72122a
[btor>main]  -std=gnu99 -W -Wall -Wextra -Wredundant-decls -O3
[btor>main] released 2021-09-24T16:45:36
[btor>main] compiled 2021-09-24T16:45:36
[btor>main] GNU 9.3.0
[btor>main] setting signal handlers
[btor>main] no time limit given
[btor>parse] assuming SMT-LIB v2 input,  parsing '/tmp/tmp3-out11.smt'
[btor>smt2] insert symbol ':all-statistics' at scope level 0
[btor>smt2] insert symbol ':authors' at scope level 0
[btor>smt2] insert symbol ':axioms' at scope level 0
[btor>smt2] insert symbol ':chainable' at scope level 0
[btor>smt2] insert symbol ':definition' at scope level 0
[btor>smt2] insert symbol ':diagnostic-output-channel' at scope level 0
[btor>smt2] insert symbol ':error-behavior' at scope level 0
[btor>smt2] insert symbol ':expand-definitions' at scope level 0
[btor>smt2] insert symbol ':extensions' at scope level 0
[btor>smt2] insert symbol ':funs' at scope level 0
[btor>smt2] insert symbol ':funs-description' at scope level 0
[btor>smt2] insert symbol ':interactive-mode' at scope level 0
[btor>smt2] insert symbol ':produce-assertions' at scope level 0
[btor>smt2] insert symbol ':language' at scope level 0
[btor>smt2] insert symbol ':left-assoc' at scope level 0
[btor>smt2] insert symbol ':name' at scope level 0
[btor>smt2] insert symbol ':named' at scope level 0
[btor>smt2] insert symbol ':notes' at scope level 0
[btor>smt2] insert symbol ':print-success' at scope level 0
[btor>smt2] insert symbol ':produce-assignments' at scope level 0
[btor>smt2] insert symbol ':produce-models' at scope level 0
[btor>smt2] insert symbol ':produce-proofs' at scope level 0
[btor>smt2] insert symbol ':produce-unsat-assumptions' at scope level 0
[btor>smt2] insert symbol ':produce-unsat-cores' at scope level 0
[btor>smt2] insert symbol ':random-seed' at scope level 0
[btor>smt2] insert symbol ':reason-unknown' at scope level 0
[btor>smt2] insert symbol ':regular-output-channel' at scope level 0
[btor>smt2] insert symbol ':right-assoc' at scope level 0
[btor>smt2] insert symbol ':sorts' at scope level 0
[btor>smt2] insert symbol ':sorts-description' at scope level 0
[btor>smt2] insert symbol ':status' at scope level 0
[btor>smt2] insert symbol ':theories' at scope level 0
[btor>smt2] insert symbol ':values' at scope level 0
[btor>smt2] insert symbol ':verbosity' at scope level 0
[btor>smt2] insert symbol ':version' at scope level 0
[btor>smt2] insert symbol ':global-declarations' at scope level 0
[btor>smt2] insert symbol '!' at scope level 0
[btor>smt2] insert symbol '_' at scope level 0
[btor>smt2] insert symbol 'as' at scope level 0
[btor>smt2] insert symbol 'DECIMAL' at scope level 0
[btor>smt2] insert symbol 'exists' at scope level 0
[btor>smt2] insert symbol 'forall' at scope level 0
[btor>smt2] insert symbol 'let' at scope level 0
[btor>smt2] insert symbol 'par' at scope level 0
[btor>smt2] insert symbol 'STRING' at scope level 0
[btor>smt2] insert symbol 'assert' at scope level 0
[btor>smt2] insert symbol 'check-sat' at scope level 0
[btor>smt2] insert symbol 'check-sat-assuming' at scope level 0
[btor>smt2] insert symbol 'declare-sort' at scope level 0
[btor>smt2] insert symbol 'declare-fun' at scope level 0
[btor>smt2] insert symbol 'declare-const' at scope level 0
[btor>smt2] insert symbol 'define-sort' at scope level 0
[btor>smt2] insert symbol 'define-fun' at scope level 0
[btor>smt2] insert symbol 'echo' at scope level 0
[btor>smt2] insert symbol 'exit' at scope level 0
[btor>smt2] insert symbol 'get-model' at scope level 0
[btor>smt2] insert symbol 'get-assertions' at scope level 0
[btor>smt2] insert symbol 'get-assignment' at scope level 0
[btor>smt2] insert symbol 'get-info' at scope level 0
[btor>smt2] insert symbol 'get-option' at scope level 0
[btor>smt2] insert symbol 'get-proof' at scope level 0
[btor>smt2] insert symbol 'get-unsat-core' at scope level 0
[btor>smt2] insert symbol 'get-unsat-assumptions' at scope level 0
[btor>smt2] insert symbol 'get-value' at scope level 0
[btor>smt2] insert symbol 'model' at scope level 0
[btor>smt2] insert symbol 'pop' at scope level 0
[btor>smt2] insert symbol 'push' at scope level 0
[btor>smt2] insert symbol 'set-logic' at scope level 0
[btor>smt2] insert symbol 'set-info' at scope level 0
[btor>smt2] insert symbol 'set-option' at scope level 0
[btor>smt2] insert symbol 'Bool' at scope level 0
[btor>smt2] insert symbol 'true' at scope level 0
[btor>smt2] insert symbol 'false' at scope level 0
[btor>smt2] insert symbol 'not' at scope level 0
[btor>smt2] insert symbol '=>' at scope level 0
[btor>smt2] insert symbol 'and' at scope level 0
[btor>smt2] insert symbol 'or' at scope level 0
[btor>smt2] insert symbol 'xor' at scope level 0
[btor>smt2] insert symbol '=' at scope level 0
[btor>smt2] insert symbol 'distinct' at scope level 0
[btor>smt2] insert symbol 'ite' at scope level 0
[btor>smt2] insert symbol 'Array' at scope level 0
[btor>smt2] insert symbol 'select' at scope level 0
[btor>smt2] insert symbol 'store' at scope level 0
[btor>smt2] insert symbol 'BitVec' at scope level 0
[btor>smt2] insert symbol 'concat' at scope level 0
[btor>smt2] insert symbol 'extract' at scope level 0
[btor>smt2] insert symbol 'bvnot' at scope level 0
[btor>smt2] insert symbol 'bvneg' at scope level 0
[btor>smt2] insert symbol 'bvand' at scope level 0
[btor>smt2] insert symbol 'bvor' at scope level 0
[btor>smt2] insert symbol 'bvadd' at scope level 0
[btor>smt2] insert symbol 'bvmul' at scope level 0
[btor>smt2] insert symbol 'bvudiv' at scope level 0
[btor>smt2] insert symbol 'bvurem' at scope level 0
[btor>smt2] insert symbol 'bvshl' at scope level 0
[btor>smt2] insert symbol 'bvlshr' at scope level 0
[btor>smt2] insert symbol 'bvult' at scope level 0
[btor>smt2] insert symbol 'bvnand' at scope level 0
[btor>smt2] insert symbol 'bvnor' at scope level 0
[btor>smt2] insert symbol 'bvxor' at scope level 0
[btor>smt2] insert symbol 'bvxnor' at scope level 0
[btor>smt2] insert symbol 'bvcomp' at scope level 0
[btor>smt2] insert symbol 'bvsub' at scope level 0
[btor>smt2] insert symbol 'bvsdiv' at scope level 0
[btor>smt2] insert symbol 'bvsrem' at scope level 0
[btor>smt2] insert symbol 'bvsmod' at scope level 0
[btor>smt2] insert symbol 'bvashr' at scope level 0
[btor>smt2] insert symbol 'repeat' at scope level 0
[btor>smt2] insert symbol 'zero_extend' at scope level 0
[btor>smt2] insert symbol 'sign_extend' at scope level 0
[btor>smt2] insert symbol 'rotate_left' at scope level 0
[btor>smt2] insert symbol 'rotate_right' at scope level 0
[btor>smt2] insert symbol 'bvule' at scope level 0
[btor>smt2] insert symbol 'bvugt' at scope level 0
[btor>smt2] insert symbol 'bvuge' at scope level 0
[btor>smt2] insert symbol 'bvslt' at scope level 0
[btor>smt2] insert symbol 'bvsle' at scope level 0
[btor>smt2] insert symbol 'bvsgt' at scope level 0
[btor>smt2] insert symbol 'bvsge' at scope level 0
[btor>smt2] insert symbol 'bvredor' at scope level 0
[btor>smt2] insert symbol 'bvredand' at scope level 0
[btor>smt2] insert symbol 'ext_rotate_left' at scope level 0
[btor>smt2] insert symbol 'ext_rotate_right' at scope level 0
[btor>smt2] insert symbol 'AUFLIA' at scope level 0
[btor>smt2] insert symbol 'AUFLIRA' at scope level 0
[btor>smt2] insert symbol 'AUFNIRA' at scope level 0
[btor>smt2] insert symbol 'LRA' at scope level 0
[btor>smt2] insert symbol 'QF_ABV' at scope level 0
[btor>smt2] insert symbol 'QF_AUFBV' at scope level 0
[btor>smt2] insert symbol 'QF_AUFLIA' at scope level 0
[btor>smt2] insert symbol 'QF_AX' at scope level 0
[btor>smt2] insert symbol 'QF_BV' at scope level 0
[btor>smt2] insert symbol 'QF_IDL' at scope level 0
[btor>smt2] insert symbol 'QF_LIA' at scope level 0
[btor>smt2] insert symbol 'QF_LRA' at scope level 0
[btor>smt2] insert symbol 'QF_NIA' at scope level 0
[btor>smt2] insert symbol 'QF_NRA' at scope level 0
[btor>smt2] insert symbol 'QF_RDL' at scope level 0
[btor>smt2] insert symbol 'QF_UF' at scope level 0
[btor>smt2] insert symbol 'QF_UFBV' at scope level 0
[btor>smt2] insert symbol 'QF_UFIDL' at scope level 0
[btor>smt2] insert symbol 'QF_UFLIA' at scope level 0
[btor>smt2] insert symbol 'QF_UFLRA' at scope level 0
[btor>smt2] insert symbol 'QF_UFNRA' at scope level 0
[btor>smt2] insert symbol 'UFLRA' at scope level 0
[btor>smt2] insert symbol 'UFNIA' at scope level 0
[btor>smt2] insert symbol 'BV' at scope level 0
[btor>smt2] insert symbol 'UFBV' at scope level 0
[btor>smt2] insert symbol 'ABV' at scope level 0
[btor>smt2] insert symbol 'ALL' at scope level 0
[btor>smt2] insert symbol 'ALL_SUPPORTED' at scope level 0
[btor>smt2] insert symbol 'v' at scope level 0
[btor>smt2] declared 'v' as bit-vector at line 1 column 16
[btor>smt2] insert symbol 'q' at scope level 0
[btor>smt2] parsed bit-vector sort of width 38
[btor>smt2] insert symbol 'p' at scope level 0
[btor>smt2] parsed bit-vector sort of width 7
[btor>smt2] insert symbol 'w' at scope level 0
[btor>smt2] remove symbol 'w' at scope level 0
[btor>smt2] remove symbol 'p' at scope level 0
[btor>smt2] remove symbol 'q' at scope level 0
[btor>smt2] parsed 2 commands in 0.00 seconds
[btor>core] calling SAT
[btor>core] found quantifiers, disable slice elimination
[btor>preprocess] no UFs or function equalities, enable beta-reduction=all
[btor>preprocess] 1 rewriting rounds in 0.0 seconds
[btor>preprocess] simplification returned 0
[btor>slvquant] enabled quant engine
[btor>core] 0/0/1/0 constraints 0/0/0/0 0.0 MB
[btor>core] 0 assumptions
[btor>core] 
[btor>core]     1 max rec. RW
[btor>core]    39 number of expressions ever created
[btor>core]    34 number of final expressions
[btor>core] 0.00 MB allocated for nodes
[btor>core]  bvconst: 1 max 1
[btor>core]  var: 1 max 1
[btor>core]  param: 4 max 5
[btor>core]  and: 20 max 20
[btor>core]  beq: 5 max 5
[btor>core]  forall: 1 max 1
[btor>core]  exists: 2 max 2
[btor>core] 
[btor>core]     0 variable substitutions
[btor>core]     0 uninterpreted function substitutions
[btor>core]     0 embedded constraint substitutions
[btor>core]     0 synthesized nodes rewritten
[btor>core]     0 linear constraint equations
[btor>core]     0 gaussian eliminations in linear equations
[btor>core]     0 eliminated sliced variables
[btor>core]     0 extracted skeleton constraints
[btor>core]     0 and normalizations
[btor>core]     0 add normalizations
[btor>core]     0 mul normalizations
[btor>core]     0 lambdas merged
[btor>core]     0 static apply propagations over lambdas
[btor>core]     0 static apply propagations over updates
[btor>core]     0 beta reductions
[btor>core]     0 clone calls
[btor>core] 
[btor>core] rewrite rule cache
[btor>core]   5 cached (add) 
[btor>core]   0 cached (get)
[btor>core]   0 updated
[btor>core]   0 removed (gc)
[btor>core]   0.00 MB cache
[btor>core] 
[btor>core] bit blasting statistics:
[btor>core]         0 AIG vectors (0 max)
[btor>core]         0 AIG ANDs (0 max)
[btor>core]         0 AIG variables
[btor>core]         0 CNF variables
[btor>core]         0 CNF clauses
[btor>core]         0 CNF literals
[btor>slvquant] 
[1]    21116 segmentation fault (core dumped)

[mpreiner]

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