smtinterpol
smtinterpol copied to clipboard
AssertionError at Theory.java:586
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)