search

ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver
GNU Lesser General Public License v3.0
61 stars 17 forks source link

AssertionError at Theory.java:586 #105

Closed rainoftime closed 5 months ago

rainoftime commented 4 years ago

Hi, for the following formula,

(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((t1 1)) ((par (T1) ((mkt1 (p1 T1))))))
(declare-datatypes ((t2 1)) ((par (T1) ((mkt2 (p1 T1))))))
(define-fun s1 () (t1 Int) (mkt1 3))
(define-fun s2 () (t2 Int) (mkt2 3))
(define-fun s3 () Int (p1 s1))
(define-fun s4 () Int (p1 s2))
(assert (= s3 s4))
(check-sat)

smtinterpol commit cb90e7441

Exception in thread "main" java.lang.AssertionError                                                                                                                                                 [6/1875]
        at de.uni_freiburg.informatik.ultimate.logic.Theory.declareInternalPolymorphicFunction(Theory.java:586)
        at de.uni_freiburg.informatik.ultimate.logic.NoopScript.declareConstructorFunctions(NoopScript.java:203)
        at de.uni_freiburg.informatik.ultimate.logic.NoopScript.declareDatatypes(NoopScript.java:221)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2730)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:1317)
        at com.github.jhoenicke.javacup.runtime.LRParser.parse(Unknown Source)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:119)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:98)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:35)
jhoenicke commented 5 months ago

Fixed. It now reports:

success
success
success
(error "test.smt2:4:20: Function p1 is already defined.")
success
success
success
(error "test.smt2:8:23: Builtin function p1 does not support argument sorts ((t2 Int))")
(error "test.smt2:9:14: Unknown function symbol s4.")
sat

I think using the same selector name in two different datatypes is not allowed by the standard.

cvc5 also complains, strangely with Cannot find unambiguous overloaded function for argument types and it doesn't complain about the doubly defined selector.