{"action":"closed","issue":{"url":"https://api.github.com/repos/juergenchrist/smtinterpol/issues/7","labels_url":"https://api.github.com/repos/juergenchrist/smtinterpol/issues/7/labels{/name}","comments_url":"https://api.github.com/repos/juergenchrist/smtinterpol/issues/7/comments","events_url":"https://api.github.com/repos/juergenchrist/smtinterpol/issues/7/events","html_url":"https://github.com/juergenchrist/smtinterpol/issues/7","id":96790140,"number":7,"title":"IndexOutOfBoundsException in ArrayValue.toSMTLIB","user":{"login":"psychon","id":89482,"avatar_url":"https://avatars.githubusercontent.com/u/89482?v=3","gravatar_id":"","url":"https://api.github.com/users/psychon","html_url":"https://github.com/psychon","followers_url":"https://api.github.com/users/psychon/followers","following_url":"https://api.github.com/users/psychon/following{/other_user}","gists_url":"https://api.github.com/users/psychon/gists{/gist_id}","starred_url":"https://api.github.com/users/psychon/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/psychon/subscriptions","organizations_url":"https://api.github.com/users/psychon/orgs","repos_url":"https://api.github.com/users/psychon/repos","events_url":"https://api.github.com/users/psychon/events{/privacy}","received_events_url":"https://api.github.com/users/psychon/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-07-23T11:17:21Z","updated_at":"2015-07-23T19:02:44Z","closed_at":"2015-07-23T19:02:44Z","body":"Input:\r\n```\r\n(set-option :print-success false)\r\n(set-option :verbosity 3)\r\n(get-info :version)\r\n(set-logic QF_ALIA)\r\n(declare-fun arr () (Array Int Int))\r\n(define-fun m0 () Int (select arr 0))\r\n(define-fun ba () Int (select arr 1))\r\n(define-fun bb () Int (select arr 2))\r\n(assert (>= (- m0 ba) 0))\r\n(assert (< (- m0 bb) 0))\r\n(check-sat)\r\n(get-model)\r\n```\r\nOutput:\r\n```\r\n(:version \"2.1-149-g744cf8f\")\r\nsat\r\nERROR - Unexpected Exception\r\njava.lang.IndexOutOfBoundsException\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.model.NumericSortInterpretation.get(NumericSortInterpretation.java:78)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.model.ArrayValue.toSMTLIB(ArrayValue.java:317)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.model.ArraySortInterpretation.get(ArraySortInterpretation.java:83)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.model.Model.toModelTerm(Model.java:270)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.model.ModelFormatter.appendFunctionValue(ModelFormatter.java:110)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.model.ModelFormatter.appendValue(ModelFormatter.java:90)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.model.Model.toString(Model.java:203)\r\n\tat java.lang.String.valueOf(String.java:2982)\r\n\tat java.io.PrintWriter.println(PrintWriter.java:754)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.printResponse(ParseEnvironment.java:211)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser$Action$.CUP$do_action(Parser.java:2043)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.Parser.do_action(Parser.java:853)\r\n\tat java_cup.runtime.LRParser.parse(Unknown Source)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseStream(ParseEnvironment.java:129)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.ParseEnvironment.parseScript(ParseEnvironment.java:114)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTLIB2Parser.run(SMTLIB2Parser.java:36)\r\n\tat de.uni_freiburg.informatik.ultimate.smtinterpol.Main.main(Main.java:180)\r\n(error \"java.lang.IndexOutOfBoundsException\")\r\n```"}}