{"action":"created","issue":{"url":"https://api.github.com/repos/newca12/gapt/issues/253","labels_url":"https://api.github.com/repos/newca12/gapt/issues/253/labels{/name}","comments_url":"https://api.github.com/repos/newca12/gapt/issues/253/comments","events_url":"https://api.github.com/repos/newca12/gapt/issues/253/events","html_url":"https://github.com/newca12/gapt/issues/253","id":55608009,"number":253,"title":"MiniSAT fails to prove deep formula of expansion proof","user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/newca12/gapt/labels/2%E2%80%935%20stars","name":"2–5 stars","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/bug","name":"bug","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Component-TheoremProvers","name":"Component-TheoremProvers","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/imported","name":"imported","color":"FFFFFF"},{"url":"https://api.github.com/repos/newca12/gapt/labels/Priority-Medium","name":"Priority-Medium","color":"FFFFFF"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":18,"created_at":"2015-01-27T11:48:04Z","updated_at":"2015-01-27T11:49:39Z","closed_at":null,"body":"_From [b.mallin...@gmx.at](https://code.google.com/u/117611913960154270727/) on November 30, 2013 19:56:14_\n\nThe test \"load veriT proofs pi and verify the validity of Deep(pi) using MiniSAT\" in MiscTest.scala:178 fails as MiniSAT claims that the formula is not valid. Prover9 is able to prove it.\r\n\r\nThe test is currently skipped. MiniSAT already fails for the second test file test1.verit\n\n_Original issue: http://code.google.com/p/gapt/issues/detail?id=253_"},"comment":{"url":"https://api.github.com/repos/newca12/gapt/issues/comments/71634543","html_url":"https://github.com/newca12/gapt/issues/253#issuecomment-71634543","issue_url":"https://api.github.com/repos/newca12/gapt/issues/253","id":71634543,"user":{"login":"newca12","id":543542,"avatar_url":"https://avatars.githubusercontent.com/u/543542?v=3","gravatar_id":"","url":"https://api.github.com/users/newca12","html_url":"https://github.com/newca12","followers_url":"https://api.github.com/users/newca12/followers","following_url":"https://api.github.com/users/newca12/following{/other_user}","gists_url":"https://api.github.com/users/newca12/gists{/gist_id}","starred_url":"https://api.github.com/users/newca12/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/newca12/subscriptions","organizations_url":"https://api.github.com/users/newca12/orgs","repos_url":"https://api.github.com/users/newca12/repos","events_url":"https://api.github.com/users/newca12/events{/privacy}","received_events_url":"https://api.github.com/users/newca12/received_events","type":"User","site_admin":false},"created_at":"2015-01-27T11:49:39Z","updated_at":"2015-01-27T11:49:39Z","body":"_From [giselle....@gmail.com](https://code.google.com/u/108711232698608960044/) on October 31, 2014 08:13:12_\n\nHi,\r\n\r\nThings are getting back on track now in Paris :)\r\nI looked at this issue and here's an update.\r\n\r\nThe comment at VeriTParser.scala:393 still holds, we ignore all the formulas of the preamble (which includes 'input', 'tmp_distinct_elim', 'tmp_alpha_conv' and 'tmp_let_elim') but the last one. This was because all these operations were doing was eliminating definitions, renaming, etc, and we did not really need the intermediary results (note that we don't even parse the let constructions - line 487). The only thing we were interested was on the final result of all these transformations, i.e., the input formula per se. \r\nWhat we did not predict was the existence of other inputs which were already in normal form and were clauses used in the proof. This is the case for the \"../testing/veriT-SMT-LIB/QF_UF/QG-classification/qg5/iso_icl419.smt2.proof_flat\" example.\r\n\r\nSince now we don't know which preamble formulas to use and which to ignore (those with 'let' and 'distinct' for example, that will still be further processed before the proof) I will do the following: all the formulas from the preamble will be stored in a hash table using their labels as a key. When parsing the proof, I will collect the clauses used and, if they are in the preamble, I will mark it as a clause used in the proof. In the end, those will be the preamble clauses that will be taken. Is it clear? Do you think it's a good solution?\r\n\r\nCheers,\r\nGiselle"}}