PAAR-2016 Fifth Workshop on Practical Aspects of Automated Reasoning July 2, 2016 Affiliated with the 8th International Joint Conference on Automated Reasoning (IJCAR 2016) Coimbra, Portugal http://cs.ru.nl/paar16/ Preface ThisvolumecontainsthepaperspresentedattheFifthWorkshoponPracticalAspectsofAutomatedReasoning (PAAR-2016). The workshop was held on July 2, 2016, in Coimbra, Portugal, in association with the Eighth International Joint Conference on Automated Reasoning (IJCAR-2016). PAAR provides a forum for developers of automated reasoning tools to discuss and compare different im- plementation techniques, and for users to discuss and communicate their applications and requirements. The workshop brought together different groups to concentrate on practical aspects of the implementation and ap- plication of automated reasoning tools. It allowed researchers to present their work in progress, and to discuss new implementation techniques and applications. Papers were solicited on topics that include all practical aspects of automated reasoning. More specifically, some suggested topics were: • automated reasoning in propositional, first-order, higher-order and non-classical logics; • implementation of provers (SAT, SMT, resolution, tableau, instantiation-based, rewriting, logical frame- works, etc); • automated reasoning tools for all kinds of practical problems and applications; • pragmatics of automated reasoning within proof assistants; • practical experiences, usability aspects, feasibility studies; • evaluation of implementation techniques and automated reasoning tools; • performance aspects, benchmarking approaches; • non-standard approaches to automated reasoning, non-standard forms of automated reasoning, new appli- cations; • implementation techniques, optimization techniques, strategies and heuristics, fairness; • support tools for prover development; • system descriptions and demos. Wewereparticularlyinterestedincontributionsthathelpthecommunitytounderstandhowtobuildusefuland powerful reasoning systems in practice, and how to apply existing systems to real problems. Wereceivedthirteensubmissions. Eachsubmissionwasreviewedbythreeprogramcommitteemembers. Due to the quality of the submissions, eleven of them were accepted. The program committee also proposed to the remaining two submissions to present their work, as presentation only. The workshop organizers would like to thank the authors and participants of the workshop, and the program committee and the reviewers for their effort. WeareverygratefultotheIJCARorganizersfortheirsupportandforhostingtheworkshop,andareindebted to the EasyChair team for the availability of the EasyChair Conference System. June 2016 Pascal Fontaine, Stephan Schulz, Josef Urban II Program Committee June Andronick (NICTA and University of New South Wales, Australia) Peter Baumgartner (NICTA/Australian National University, Australia) Christoph Benzmu¨ller (Freie Universit¨at Berlin, Germany) Armin Bierre (Johannes Kepler University, Austria) Nikolaj Bjorner (Microsoft Research, USA) Simon Cruanes (Loria, INRIA, France) Hans de Nivelle (University of Wroclaw, Poland) Pascal Fontaine (Loria, INRIA, University of Lorraine, France), co-chair Vijay Ganesh (University of Waterloo, Canada) Alberto Griggio (FBK-IRST, Italy) John Harrison (Intel, USA) Marijn Heule (The University of Texas at Austin, USA) Dejan Jovanovi´c (SRI International, USA) Yevgeny Kazakov (The University of Ulm, Germany) Chantal Keller (LRI, Universit´e Paris-Sud, France) Boris Konev (The University of Liverpool, UK) Konstantin Korovin (The University of Manchester, UK) Laura Kovacs (Chalmers University, Sweden) Jens Otten (University of Potsdam, Germany) Nicolas Peltier (CNRS - LIG, France) Ruzica Piskac (Yale University, USA) Giles Reger (The University of Manchester, UK) Andrew Reynolds (EPFL, Switzerland) Philipp Ruemmer (Uppsala University, Sweden) Uli Sattler (The University of Manchester, UK) Renate A. Schmidt (The University of Manchester, UK) Stephan Schulz (DHBW Stuttgart, Germany), co-chair Geoff Sutcliffe (University of Miami, USA) Josef Urban (Czech Technical University in Prague, Czech Republic), co-chair Uwe Waldmann (MPI Saarbru¨cken, Germany) External reviewers Peter Backeman Murphy Berzish Chad Brown Yizheng Zhao III Table of Contents Efficient Instantiation Techniques in SMT (Work In Progress) . . . . . . . . . . . . . . . . . . . . . . . . . 1 Haniel Barbosa Alternative treatments of common binary relations in first-order automated reasoning . . . . . . . . . . . 11 Koen Claessen and Ann Lilliestr¨om No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions . . . . . . . . . . . . . . 24 Michael F¨arber and Cezary Kaliszyk Deduction as a Service . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Mohamed Hassona and Stephan Schulz TH1: The TPTP Typed Higher-Order Form with Rank-1 Polymorphism. . . . . . . . . . . . . . . . . . . 41 Cezary Kaliszyk, Geoff Sutcliffe and Florian Rabe Prover-independent Axiom Selection for Automated Theorem Proving in Ontohub . . . . . . . . . . . . . 56 Eugen Kuksa and Till Mossakowski On Checking Kripke Models for Modal Logic K . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 Jean Marie Lagniez, Daniel Le Berre, Tiago de Lima and Valentin Montmirail Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers . . . . . . . . . . 82 Tomer Libal and Alexander Steen Ordered Resolution with Straight Dismatching Constraints . . . . . . . . . . . . . . . . . . . . . . . . . . 95 Andreas Teucke and Christoph Weidenbach A Saturation-based Algebraic Reasoner for ELQ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110 Jelena Vlasenko, Maryam Daryalal, Volker Haarslev and Brigitte Jaumard The PIE Environment for First-Order-Based Proving, Interpolating and Eliminating . . . . . . . . . . . . 125 Christoph Wernhard IV Efficient Instantiation Techniques in SMT (Work In Progress) Haniel Barbosa∗ LORIA, INRIA, Universit´e de Lorraine, Nancy, France [email protected] Abstract In SMT solving one generally applies heuristic instantiation to handle quantified formulas. This has the side effect of producing many spuri- ous instances and may lead to loss of performance. Therefore deriving bothfewerandmoremeaningfulinstancesaswellaseliminatingordis- missing, i.e., keeping but ignoring, those not significant for the solving are desirable features for dealing with first-order problems. This paper presents preliminary work on two approaches: the imple- mentation of an efficient instantiation framework with an incomplete goal-oriented search; and the introduction of dismissing criteria for heuristic instances. Our experiments show that while the former im- proves performance in general the latter is highly dependent on the problem structure, but its combination with the classic strategy leads to competitive results w.r.t. state-of-the-art SMT solvers in several benchmark libraries. 1 Introduction SMTsolvers(see[4]forageneralpresentationofSMT)areextremelyefficientathandlinglargegroundformulas with interpreted symbols, but they still struggle to deal with quantified formulas. Quantified first-order logic is besthandledwithResolution andSuperposition-basedtheoremproving[2,16]. Althoughtherearefirstattempts tounifysuchtechniqueswithSMT[13],themainapproachusedinSMTisstillinstantiation: formulasarefreed from quantifiers and refuted with the help of decision procedures for ground formulas. ThemostcommonstrategyforfindinginstancesinSMTistheuseoftriggers [10]: sometermsinaquantified formulaareselectedtobeinstantiatedandsuccessfullydoingsoprovidesagroundinstantiationfortheformula. These triggers are selected according to various heuristics and instantiated by performing E-matching over candidate terms retrieved from a ground model. The lack of a goal in this technique (such as, e.g., refuting the model) leads to the production of many instances not relevant for the solving. Furthermore, unlike other non-goal-oriented techniques, such as superposition, there are no straightforward redundancy criteria for the elimination of derived instances in SMT solving. Therefore useless instances are kept, potentially hindering the solver’s performance. Our attempt to tackle this issue is two-fold: • A method for deriving fewer instances by setting the refutation of the current model as a goal, as in [19]. Thus all instances produced by this strategy are relevant. ∗This work has been partially supported by the ANR/DFG project STU 483/2-1 SMArT, project ANR-13-IS02-0001 of the AgenceNationaledelaRecherche Copyright (cid:13)c by the paper’s authors. Copying permitted for private and academic purposes. In: P. Fontaine, S. Schulz, J. Urban (eds.): Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR2016),Coimbra,Portugal,02-07-2016,publishedathttp://ceur-ws.org 1 • Heuristicinstantiationiskeptundercontrol. Giventheirspeedandthedifficultyofthefirst-orderreasoning with interpreted symbols, heuristics are a necessary evil. To reduce side effects, spurious instances are dismissed. The criterion is their activity as reported by the ground solver, in a somehow hybrid approach avoiding both the two-tiered combination of SAT solvers [12] and deletion [7]. Wealsointroducealiftingoftheclassiccongruenceclosureproceduretofirst-orderlogicandshowitssuitability asthebasisofourinstantiationtechniques. Moreover,itisshownhowtechniquescommoninfirst-ordertheorem proving are being implemented in an SMT setting, such as using efficient term indexing and performing E- unification. Formal preliminaries Duetospaceconstraints,werefertotheclassicnotionsofmany-sortedfirst-orderlogicwithequalityasthebasis for the notation in this paper. Only the most relevant are mentioned. Given a set of ground terms T and a congruence relation (cid:39) on T, a congruence C over T is a set C ⊆{s(cid:39) t | s,t ∈ T} closed under entailment: for all s,t ∈ T, C |= s (cid:39) t iff s (cid:39) t ∈ C. The congruence closure of C is the least congruence on T containing C. Given a consistent set of ground equality literals E, two terms t ,t 1 2 are said congruent iff E |=t (cid:39)t , which amounts to t (cid:39)t being in the congruence closure of the equalities in 1 2 1 2 E, and disequal iff E |=t (cid:54)(cid:39)t . The congruence class of a given term t, represented by [t], is the partition of T 1 2 induced by E in which all terms are congruent to t. 2 Congruence Closure with Free Variables TobetterhandlethequantifiedformulasduringinstantiationalgorithmswehavedevelopedaCongruenceClosure with Free Variables (CCFV, for short), which extends the classic congruence closure procedure [14, 15] into handlingconjunctionsofequalityliteralswithfreevariables, performingrigid E-unification: findingsolutionsto agivensetofequationsconsistentwithasetofequationsE, assumingthateveryvariabledenotesasingleterm. L, x(cid:39)y(cid:107)U (RV) (i) (cid:39)∈{(cid:39),(cid:54)(cid:39)} L(cid:107)U∪{x(cid:39)y} (ii) x or y is free in U, or E∪U |=x(cid:39)y L, x(cid:39)t(cid:107)U (RT) (i) (cid:39)∈{(cid:39),(cid:54)(cid:39)} L(cid:107)U∪{x(cid:39)t} (ii) either x is free in U or E∪U |=x(cid:39)t L,f(u)(cid:39)f(v)(cid:107)U L(cid:107)U (Decompose) (Yield) (i) L=∅ or E |=L L,u(cid:39)v(cid:107)U (cid:62) L, f(u)(cid:39)t(cid:107)U (Ematch) (i) (cid:39)∈{(cid:39),(cid:54)(cid:39)} L, f(u)(cid:39)f(t1)(cid:107)U (ii) f(t ) are ground terms from E ... i (iii) E |=t(cid:39)f(t ), for 1≤i≤n L, f(u)(cid:39)f(tn)(cid:107)U i L, u(cid:39)f(u(cid:48))(cid:107)U (Euni) (i) (cid:39)∈{(cid:39),(cid:54)(cid:39)} L, u(cid:39)t1,1, f(u(cid:48))(cid:39)f(t(cid:48)1)(cid:107)U (ii) ti,j, f(t(cid:48)i) are ground terms ... from E L, u(cid:39)t1,m1, .f.(.u(cid:48))(cid:39)f(t(cid:48)1)(cid:107)U (iii) E |=ti,j (cid:39)f(t(cid:48)i), L, u(cid:39)tn,mn, f(u(cid:48))(cid:39)f(t(cid:48)n)(cid:107)U for 1≤i≤n, 1≤j ≤mi L(cid:107)U (Close) (i) L is inconsistent modulo E or no other ⊥ rule can be applied Table 1: CCFV calculus for solving rigid E-unification in equational FOL. Multiple conclusion rules represent branching in the search. x,y refer to variables, t to ground terms, u to non-ground terms and v to terms in general. 2 Our procedure implements the rules1 shown in Table 1. To simplify presentation, it is assumed, without loss of generality, that function symbols are unary. Rules are shown only for equality literals, as their extension into uninterpreted predicates is straightforward. The calculus operates on conjunctive sets of equality literals containingfreevariables,annotatedwithequalityliteralsbetweenthesevariablesandgroundtermsorthemselves. Initiallytheannotationsareempty,beingaugmentedastherulesareappliedandtheinputproblemissimplified, embodying its solution. CCFV algorithm Given a set of ground equality literals E and a set of non ground equality literals L whose free variables are X, CCFV computes sets of equality literals U ,...,U , denoted unifiers. Each unifier associates variables from X 1 n to ground terms and allows the derivation of ground substitutions σ ,...,σ such that E |=Lσ , if any: 1 k i (cid:26) (cid:27) x(cid:55)→t x∈X; U |=x(cid:39)t for some ground term t. If x is free σ = i in U, t is a ground term selected from its sort class. SincenotnecessarilyallvariablesinX arecongruenttogroundtermsinagivenunifierU (denoted“freeinU”), more than one ground substitution may be obtained by assigning those variables to different ground terms in their sort classes. A terminating strategy for CCFV is to apply the rules of Table 1 exhaustively over L, except that Ematch may not be applied over the literals it introduces. There must be a backtracking when a given branch results in Close, until being able to apply Yield. In those cases a unifier is provided from which substitutions solving the given E-unification problem can be extracted. Term Indexing PerformingE-unificationrequiresdealingwithmanyterms,whichmakestheuseofanefficientindexingtechnique for fast retrieval of candidates paramount. The Congruence Closure procedure in veriT keeps a signature table, in which terms and predicate atoms are kept modulo their congruence classes. For instance, if a (cid:39) b and both f(a) and f(b) appear in the formula, only f(a) is kept in the signature table. Those are referred to as signatures and are the only relevant terms for indexing, since instantiations into terms with the same signature are logically equivalent modulo the equalities in the current context. The signature table is indexed by top symbol2, such that each function and predicate symbol points to all their related signatures. Those are kept sorted by congruence classes, to be amenable for binary search. Bitmasks are kept to fast check whether a class contains signatures with a given top symbol, a necessary condition for retrieving candidates from that class. Asideeffectofbuildingthetermindexfromthesignaturetableisthatall terms areconsidered, regardlessof whether they appear or not in the current SAT solver model. To tackle this issue, an alternative index is built directlyfromthecurrentlyassertedliteralswhilecomputingontheflytherespectivesignatures. Dealingdirectly with the model also has the advantage of allowing its minimization, since the SAT solver generally asserts more literals than necessary. Computing a prime implicant, a minimal partial model, can be done in linear time [9]. Moreover, the CNF overhead is also cleaned: removing literals introduced by the non-equivalency preserving CNF transformation the formula undergoes, applying the same process described in [7] for Relevancy. Implementing E-unification The main data structure for CCFV is the “unifiers”: for a set of variables X, an array with each position representing a valuation for a variable x∈X, which consists of: • a field for the respective variable; • a flag to whether that variable is the representative of its congruence class; • a field for, if the variable is a representative, the ground term it is equal to and a set of terms it is disequal to; otherwise a pointer to the variable it is equal to, the default being itself. 1Thecalculusstillneedstobeimproved,withabetterpresentationandtheproofsofitsproperties,whichareworkinprogress. 2Sincetopsymbolindexingisnotoptimal,thenextstepistoimplementfingerprintindexing. Thecurrentimplementationkeeps theindexingasmodularaspossibletofacilitateeventuallychangingitsstructure. 3 EachunifierrepresentsoneofthesetsU mentionedabove. TheyarehandledwithaUNION-FINDalgorithm with path-compression. The union operation is made modulo the congruence closure on the ground terms and the current assignments to the variables in that unifier, which maintains the invariant of it being a consistent set of equality literals. TherulesinTable1areimplementedasanadaptationoftherecursive descent E-unification algorithmin[1], heavily depending on the term index described shown above for optimizing the search. Currently it does not have a dedicated index for performing unification, rather relying in the DAG structure of the terms. To avoid (usually expensive) re-computations, memoization is used to store the results of E-unifications attempts, which is particularly useful when looking for unifiers for, e.g., f(x)(cid:39)g(y) in which both “f” and “g” have large term indexes. Fornowthese“unificationjobs”areindexedbytheliteral’spolarityandparticipatingterms,nottaking into account their structure. 3 Instantiation Framework 3.1 Goal-oriented instantiation In the classic architecture of SMT solving, a SAT solver enumerates boolean satisfiable conjunctions of literals to be checked for ground satisfiability by decision procedures for a given set of theories. If these models are not refuted at the ground level they must be evaluated at the first-order level, which is not a decidable problem in general. Therefore one cannot assume to have an efficient algorithm to analyze the whole model and determine if it can be refuted. This led to the regular heuristic instantiation in SMT solving being not goal-oriented: its search is based solely on pattern matching of selected triggers [10], without further semantic criteria, which can be performed quickly and then revert the reasoning back to the efficient ground solver. In [19], Reynolds et al. presented an efficient incomplete goal-oriented instantiation technique that evaluates a quantified formula, independently, in search for conflicting instances: given a satisfiable conjunctive set of groundliteralsE, asetofquantifiedformulasQandsome∀x.ψ ∈Qitsearchesforagroundsubstitutionσ such that E |= ¬ψσ. Such substitutions are denoted ground conflicting, with conflicting instances being such that ∀x.ψ →ψσ refutes E∪Q. Since the existence of such substitutions is an NP-complete problem equivalent to Non-simultaneous rigid E-unification [20], the CCFV procedure is perfectly suited to solve it. Each quantified formula ∀x.ψ ∈ Q is converted into CNF and CCFV is applied for computing sequences of substitutions3 σ ,...,σ such that, for 0 k ¬ψ =l ∧···∧l , 1 k σ =∅; σ ⊆σ and E |=l σ 0 i−1 i i i which guarantees that E |= ¬ψσ and that the instantiation lemma ∀x.ψ → ψσ refutes E∪Q. If any literal k k l is not unifiable according to the unifications up to l , there are no conflicting instances for ∀x.ψ. i+i i Currently our implementation applies a breadth-first search on the conjunction of non-ground literals, com- puting all unifiers for a given literal l ∈ ¬ψ before considering the next one. Memory consumption is an issue due to the combinatorial explosion that might occur when merging sets of unifiers from different literals. A more general issue is simply the time required for finding the unifiers of a given literal, which can have a huge search space depending on the number of indexed terms. To minimize these problems customizable parameters set thresholds both on the number of potential combinations and of terms to be considered. 3.2 Heuristic instantiation with instances dismissal Althoughgoal-orientedsearchavoidsheuristicinstantiationinmanycases,triggersandpattern-matchingarestill the backbone of our framework. A well known side effect of them is the production of many spurious instances which not only interfere with the performances of both the ground and instantiation modules but also may lead to matching loops: triggers generating instances which are used solely to produce new instances in an infinite chain. To avoid this issues, de Moura et al. [7] mention how they perform clause deletion, during backtracking, ofinstanceswhichwerenotpartofaconflict. However,thisprovedtobeanengineeringchallengeinveriT,since its original architecture does not easily allow deletion of terms from the ground solver. 3Since CCFV is non-proof confluent calculus, as choices may need to be made whenever a matching or unification must be performed,backtracksareusuallynecessaryforexploringdifferentoptions. 4 To circumvent this problem, instead of being truly deleted instances are simply dismissed: by labeling them with instantiation levels4, at a given level n only instances whose level is at most n−1 are considered. This is done by using the term indexing from the SAT model and eliminating literals whose instantiation level is above the threshold. At each instantiation round, the level is defined as the current level plus one. At the beginning of the solving all clauses are assigned level 0, the starting value for the instantiation level. At the end of an instantiation round, the SAT solver is notified that at that point in the decision tree there was an instantiation, so that whenever there is a backtracking to a point before such a mark the instantiation level is decremented, at the same time that all instances which have participated in a conflict are promoted to “level 0”. This ensures that those instances will not be dismissed for instantiation, which somehow emulates clause deletion. With this technique, however, the ground solver will still be burdened by the spurious instances, but they also will not need to be regenerated in future instantiation rounds. ... ... ⊥ I1 I1(cid:48) ⊥ ... 1 I ... 2 ⊥2 I2(cid:48) ⊥ 3 Figure 1: Example of instance dismissal ConsiderinFigure1anexampleofinstancedismissal. I marksaninstantiationhappeningatlevel1,inwhich 1 all clauses from the original formula are considered for instantiation. Those lead to a conflict and a backtrack to a point before I , which decrements the instantiation level to 0. All instances from I which were part of the 1 1 conflict in ⊥ are promoted to level 0, the rest kept with level 1. At I only terms in clauses with level 0 are 1 1(cid:48) indexed. Since subsequently there is no backtracking to a point before I , the instantiation level is increased to 1(cid:48) 1. AtI allclausesoflevel1areconsidered,thusincludingthoseproducedbothinI andI . Afterabacktrack, 2 1 1(cid:48) the level is decremented to 1 and the instances participating in ⊥ are promoted. This way at I only the 2 2(cid:48) promotedinstancesfromthepreviousroundareconsidered. Thenthegroundsolverreachesaconflictin⊥ and 3 cannot produce any more models, concluding unsatisfiability. 4 Experiments The above techniques have been implemented in the SMT solver veriT [6], which previously offered support for quantified formulas solely through na¨ıve trigger instantiation, without further optimizations5. The evaluation was made on the “UF”, “UFLIA”, “UFLRA” and “UFIDL” categories of SMT-LIB [5], which have 10,495 benchmarks annotated as unsatisfiable. They consist mostly of quantified formulas over uninterpreted functions as wellas equality andlinear arithmetic. Thecategories withbit vectors andnon-linear arithmeticare currently notsupportedbyveriTandinthoseinwhichuninterpretedfunctionsarenotpredominantthetechniquesshown here are not quite as effective yet. Our experiments were conducted using machines with 2 CPUs Intel Xeon E5-2630 v3, 8 cores/CPU, 126GB RAM, 2x558GB HDD. The timeout is set for 30 seconds, since our goal is evaluating SMT solvers as backends of verification and ITP platforms, which require fast answers. The different configurations of veriT are identified in this section according to which techniques they have activated: • veriT: the solver relying solely on na¨ıve trigger instantiation; • veriT i: the solver with CCFV and the signature table indexed; • veriT ig: besides the above, uses the goal-oriented search for conflicting instances; 4Thisisdonemuchinthespiritof[11],althoughtheirlabelingdoesnottakeintoaccounttheinteractionswiththeSATsolver andisaimedatpreventingmatchingloops,nottowards“deletion”. 5Adevelopmentversionisavailableathttp://www.loria.fr/~hbarbosa/veriT-ccfv.tar.gz 5 • veriT igd: does the term indexing from the SAT solver and uses the goal-oriented search and instance dismissal. Figure 2a shows the big impact of the handling of instantiation by CCFV: veriT i is significantly faster and solves 326 problems exclusively, while the old configuration solves only 32 exclusively. Figure 2b presents a significant improvement in terms of problems solved (474 more against 36 less) by the use of the goal-oriented instantiation, but it also shows a less clear gain of time. Besides the natural chaotic behavior of trigger instan- tiation, we believe this is due to the more expensive search performed: trying to falsify quantified formulas and handling E-unification, which, in the context of SMT, has a much bigger search space than simply performing E-matching for pattern-matching instantiation. Not always the “better quality” of the conflicting instances off- sets the time it took to compute them, which indicates the necessity of trying to identify beforehand such cases and avoid the more expensive search when counter-producent. 11110000 11110000 veriT_iveriT_iveriT_iveriT_i veriT_igveriT_igveriT_igveriT_ig 1111 1111 0000....1111 0000....1111 0000....1111 1111 11110000 0000....1111 1111 11110000 vvvveeeerrrriiiiTTTT vvvveeeerrrriiiiTTTT____iiii (a) Impact of CCFV, without goal-oriented instantiation (b) Impact of goal-oriented instantiation Figure 2: Comparisons of new term indexing, CCFV and goal-oriented search Logic Class CVC4 Z3 veriT igd veriT ig veriT i veriT grasshopper 410 418 431 437 418 413 UF sledgehammer 1412 1249 1293 1272 1134 1066 UFIDL all 61 62 56 58 58 58 boogie 841 852 722 681 660 661 sexpr 15 26 15 7 5 5 UFLIA grasshopper 320 341 356 367 340 335 sledgehammer 1892 1581 1781 1778 1620 1569 simplify 770 831 797 803 735 690 simplify2 2226 2337 2277 2298 2291 2177 Total 7947 7697 7727 7701 7203 6916 Table 2: Comparison between instantiation based SMT solvers on SMT-LIB benchmarks Our new implementations were also evaluated against the SMT solvers Z3 [8] (version 4.4.2) and CVC4 [3] (version1.5),bothbasedoninstantiationforhandlingquantifiedformulas. TheresultsaresummarizedinTable2, excluding categories whose problems are trivially solved by all systems, which leaves 8,701 for consideration. WhileveriT igandveriT igdsolveasimilarnumberofproblemsinthesamecategories(withasmalladvantage tothelatter),itshouldbenotedthattheyhavequitediverseresultsdependingonthebenchmark(acomparison is shown in Figure 4 at Appendix A). Each configuration solves ≈ 150 problems exclusively. This indicates the potential to use both the term indexes, from the signature table and from the SAT solver model with instance dismissal, during the solving. Regarding overall performance, CVC4 solves the most problems, being the more robust SMT solver for instantiationandalsoapplyingagoal-orientedsearchforconflictinginstances. BothconfigurationsofveriTsolve approximately the same number of problems as Z3, although mostly because of the better performance on the 6