smtinterpol icon indicating copy to clipboard operation
smtinterpol copied to clipboard

AssertionError at Theory.java:586

Open rainoftime opened this issue 4 years ago • 0 comments

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)

rainoftime avatar Jul 02 '20 08:07 rainoftime