Bitwuzla Parsing Symbols Twice With Error

[baierd]

Bitwuzla parses a symbol twice and throws an error when parsing the following SMTLIB2 queries in order:

(declare-const |main::b@3| (_ BitVec 32))
(declare-const |main::a@4| (_ BitVec 32))
(declare-const |main::c@2| (_ BitVec 32))
(define-fun @def0 () Bool (= |main::a@4| #b00000000000000000000000000001010))
(assert (and (and (and @def0 (not @def0)) (bvsle |main::b@3| #b00000000000000000000000000000101)) (not (= |main::c@2| #b00000000000000000000000000000000))))

(declare-const |main::a@3| (_ BitVec 32))
(declare-const |main::a@4| (_ BitVec 32))
(assert (and (not (= |main::a@3| #b00000000000000000000000000001010)) (= |main::a@4| (bvadd |main::a@3| #b00000000000000000000000000000001))))

(declare-const nondet_int!2@ (_ BitVec 32))
(declare-const |main::nondet@3| (_ BitVec 32))
(declare-const |main::a@3| (_ BitVec 32))
(declare-const nondet_int!3@ (_ BitVec 32))
(declare-const |main::b@3| (_ BitVec 32))
(assert (and (and (and (= |main::nondet@3| nondet_int!2@) (= |main::a@3| #b00000000000000000000000000000000)) (= |main::b@3| nondet_int!3@)) (not (= |main::nondet@3| #b00000000000000000000000000000000))))

(assert false)

(assert false)

Exception in CPAchecker:

java.lang.IllegalArgumentException: <string>:11:14: symbol '|main::nondet@3|' already defined at line 2 column 14
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.BitwuzlaNativeJNI.Parser_parse__SWIG_0(Native Method)
	at org.sosy_lab.java_smt.solvers.bitwuzla.api.Parser.parse(Unknown Source)
	at org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormulaManager.parseImpl(BitwuzlaFormulaManager.java:126)
	at org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormulaManager.parseImpl(BitwuzlaFormulaManager.java:28)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.parse(AbstractFormulaManager.java:330)
	at org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.translateFrom(AbstractFormulaManager.java:488)
	at org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.translateFrom(FormulaManagerView.java:1913)

Triggering Command-line: --bmc-interpolation --option imc.fallBack=false --option solver.solver=BITWUZLA --option solver.interpolationSolver=MATHSAT5 --option cpa.predicate.encodeIntegerAs=BITVECTOR --timelimit 60s --option solver.enableLoggingInSolver=true --option solver.logAllQueries=true --spec test/config/properties/unreach-label.prp test/programs/simple/automata_test.c

[daniel-raffler]

This is a known issue and we already have an open PR here

[baierd]

This is a known issue and we already have an open PR here

You mean this is the late issue for the PR ;D

Thanks for adding the link and the reminder!