% Publication metadata only. Reading scope and implementation status belong in the paper notes.
% Initial matching entries imported from a user-supplied bibliography; identifiers and editions normalized.

@inbook{deMoura2013,
    title = {The Strategy Challenge in {SMT} Solving},
    isbn = {9783642366758},
    issn = {1611-3349},
    url = {https://doi.org/10.1007/978-3-642-36675-8_2},
    doi = {10.1007/978-3-642-36675-8_2},
    booktitle = {Automated Reasoning and Mathematics},
    publisher = {Springer Berlin Heidelberg},
    author = {de Moura, Leonardo and Passmore, Grant Olney},
    year = {2013},
    pages = {15--44}
}

@inproceedings{deharbe2011symmetry,
    title = {Exploiting Symmetry in {SMT} Problems},
    author = {D{\'e}harbe, David and Fontaine, Pascal and Merz, Stephan and Woltzenlogel Paleo, Bruno},
    booktitle = {Automated Deduction -- CADE-23},
    year = {2011},
    url = {https://www.verit-solver.org/papers/cade2011.pdf}
}

@inproceedings{areces2013symt,
    title = {{SyMT}: Finding Symmetries in {SMT} Formulas},
    author = {Areces, Carlos and D{\'e}harbe, David and Fontaine, Pascal and Orbe, Ezequiel},
    booktitle = {Proceedings of the 11th International Workshop on Satisfiability Modulo Theories},
    year = {2013},
    note = {Work in progress},
    url = {https://members.loria.fr/PFontaine/Areces3.pdf}
}

@misc{dingliwal2020symmetry,
    title = {Advances in Symmetry Breaking for {SAT} Modulo Theories},
    author = {Dingliwal, Saket and Agarwal, Ronak and Mittal, Happy and Singla, Parag},
    year = {2020},
    note = {arXiv:1908.00860, version 2},
    doi = {10.48550/arXiv.1908.00860},
    url = {https://arxiv.org/abs/1908.00860v2}
}

@incollection{margot2010symmetry,
    title = {Symmetry in Integer Linear Programming},
    author = {Margot, Fran{\c{c}}ois},
    booktitle = {50 Years of Integer Programming 1958--2008},
    publisher = {Springer},
    year = {2010},
    pages = {647--686},
    doi = {10.1007/978-3-540-68279-0_17}
}

@misc{bodi2011symmetry,
    title = {Algorithms for Highly Symmetric Linear and Integer Programs},
    author = {B{\"o}di, Richard and Herr, Katrin and Joswig, Michael},
    year = {2011},
    note = {arXiv:1012.4941, version 2},
    doi = {10.48550/arXiv.1012.4941},
    url = {https://arxiv.org/abs/1012.4941v2}
}

@inproceedings{BjornerN24,
    author = "Bj{\o}rner, Nikolaj S. and Nachmanson, Lev",
    title = "Arithmetic Solving in {Z3}",
    booktitle = "Computer Aided Verification - 36th International Conference, {CAV}",
    volume = "14681",
    pages = "26--41",
    publisher = "Springer",
    year = "2024",
    doi = "10.1007/978-3-031-65627-9_2"
}

@article{MouraB08,
    author = "de Moura, Leonardo Mendon{\c{c}}a and Bj{\o}rner, Nikolaj S.",
    title = "Model-based Theory Combination",
    volume = "198",
    number = "2",
    pages = "37--49",
    publisher = "Elsevier",
    year = "2008",
    doi = "10.1016/J.ENTCS.2008.04.079",
    journal = "Electronic Notes in Theoretical Computer Science"
}

@inproceedings{Jon2017,
    author = "Jon\'{a}\v{s}, Martin and Strej\v{c}ek, Jan",
    title = "On Simplification of Formulas with Unconstrained Variables and Quantifiers",
    doi = "10.1007/978-3-319-66263-3_23",
    url = "https://www.fi.muni.cz/~xstrejc/publications/sat2017preprint.pdf",
    booktitle = "Theory and Applications of Satisfiability Testing – SAT 2017",
    publisher = "Springer International Publishing",
    year = "2017",
    pages = "364--379"
}

@article{Andersen1995,
    author = "Andersen, Erling D. and Andersen, Knud D.",
    title = "Presolving in linear programming",
    volume = "71",
    doi = "10.1007/bf01586000",
    number = "2",
    journal = "Mathematical Programming",
    publisher = "Springer Science and Business Media LLC",
    year = "1995",
    month = "December",
    pages = "221--245"
}

@inproceedings{Brummayer2009,
    author = "Brummayer, Robert and Biere, Armin",
    booktitle = "Proceedings of the 7th International Workshop on Satisfiability Modulo Theories",
    month = "August",
    pages = "1--5",
    publisher = "ACM",
    series = "SMT '09",
    title = "Fuzzing and delta-debugging {SMT} solvers",
    year = "2009",
    doi = "10.1145/1670412.1670413"
}

@inproceedings{DutertreM06,
    author = "Dutertre, Bruno and de Moura, Leonardo Mendon{\c{c}}a",
    booktitle = "Computer Aided Verification, 18th International Conference, {CAV} 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings",
    pages = "81--94",
    publisher = "Springer",
    series = "Lecture Notes in Computer Science",
    title = "A Fast Linear-Arithmetic Solver for {DPLL(T)}",
    volume = "4144",
    year = "2006",
    doi = "10.1007/11817963_11"
}

@phdthesis{griggio2009,
    author = "Griggio, Alberto",
    school = "University of Trento",
    title = "An Effective {SMT} Engine for Formal Verification",
    doi = "10.15168/11572_368265",
    year = "2009"
}

@phdthesis{king2014,
    author = "King, Tim",
    pages = "247",
    school = "New York University",
    title = "Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic",
    year = "2014",
    url = "https://cs.nyu.edu/media/publications/king_tim.pdf"
}

@inproceedings{Monniaux2009,
    author = "Monniaux, David",
    booktitle = "Computer Aided Verification",
    pages = "570--583",
    publisher = "Springer Berlin Heidelberg",
    title = "On Using Floating-Point Computations to Help an Exact Linear Arithmetic Decision Procedure",
    year = "2009",
    doi = "10.1007/978-3-642-02658-4_42"
}

@inproceedings{sorensson2009minimizing,
    author = {S{\"o}rensson, Niklas and Biere, Armin},
    title = {Minimizing Learned Clauses},
    booktitle = {Theory and Applications of Satisfiability Testing -- SAT 2009},
    year = {2009},
    pages = {237--243},
    doi = {10.1007/978-3-642-02777-2_23},
    url = {https://cca.informatik.uni-freiburg.de/papers/SoerenssonBiere-SAT09.pdf}
}

@inproceedings{feng2020alluip,
    author = {Feng, Nick and Bacchus, Fahiem},
    title = {Clause Size Reduction with all-{UIP} Learning},
    booktitle = {Theory and Applications of Satisfiability Testing -- SAT 2020},
    year = {2020},
    pages = {28--45},
    doi = {10.1007/978-3-030-51825-7_3},
    url = {https://pmc.ncbi.nlm.nih.gov/articles/PMC7326470/}
}

@techreport{fleury2021alluip,
    author = {Fleury, Mathias and Biere, Armin},
    title = {Efficient All-{UIP} Learned Clause Minimization (Extended Version)},
    institution = {Johannes Kepler University Linz},
    number = {21/3},
    year = {2021},
    doi = {10.35011/fmvtr.2021-3},
    url = {https://fmv.jku.at/papers/FleuryBiere-FMV-TR-21-3.pdf}
}

@inproceedings{vangelder2009minimization,
    author = {Van Gelder, Allen},
    title = {Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces},
    booktitle = {Theory and Applications of Satisfiability Testing -- SAT 2009},
    year = {2009},
    pages = {141--146},
    doi = {10.1007/978-3-642-02777-2_15},
    url = {https://users.soe.ucsc.edu/~avg/Papers/ccmin-avg-sat09.pdf}
}

@inproceedings{King-fmcad2013,
    author = "King, Tim and Barrett, Clark and Dutertre, Bruno",
    booktitle = "2013 Formal Methods in Computer-Aided Design",
    month = "October",
    pages = "189--196",
    publisher = "IEEE",
    title = "Simplex with sum of infeasibilities for {SMT}",
    year = "2013",
    doi = "10.1109/fmcad.2013.6679409"
}

@inproceedings{yices2,
    author = "Dutertre, Bruno",
    title = "Yices 2.2",
    booktitle = "Computer Aided Verification - 26th International Conference, {CAV} 2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna, Austria, July 18-22, 2014. Proceedings",
    series = "Lecture Notes in Computer Science",
    volume = "8559",
    pages = "737--744",
    publisher = "Springer",
    year = "2014",
    doi = "10.1007/978-3-319-08867-9_49"
}

@inproceedings{janota2026primo,
    author = "Janota, Mikol{\'{a}}{\v{s}} and Jakub{\r{u}}v, Jan",
    title = "Vibe-Coded and Tuned: A State-of-the-Art {SMT} Solver for {QF-LRA}",
    booktitle = "Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers)",
    editor = "Schulz, Stephan and Korovin, Konstantin and Rawson, Michael",
    series = "Kalpa Publications in Computing",
    volume = "23",
    pages = "44--56",
    publisher = "EasyChair",
    year = "2026",
    issn = "2515-1762",
    doi = "10.29007/rn52",
    url = "https://easychair.org/publications/paper/rPZ9"
}

@misc{janota2026vibecodedtunedstateoftheartsmt,
    author = "Janota, Mikol{\'{a}}{\v{s}} and Jakub{\r{u}}v, Jan",
    title = "Vibe-Coded and Tuned: A State-of-the-Art {SMT} Solver for {QF-LRA}",
    year = "2026",
    eprint = "2609.16706",
    archiveprefix = "arXiv",
    primaryclass = "cs.LO",
    url = "https://arxiv.org/abs/2609.16706"
}

@phdthesis{bromberger2019,
    author = "Bromberger, Martin",
    title = "Decision Procedures for Linear Arithmetic",
    school = "Universität des Saarlandes",
    year = "2019",
    url = "https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28955"
}

@phdthesis{brummayer2009thesis,
    author = "Brummayer, Robert Daniel",
    title = "Efficient {SMT} Solving for Bit-Vectors and the Extensional Theory of Arrays",
    school = "Johannes Kepler University Linz",
    year = "2009",
    url = "https://research.jku.at/en/publications/efficient-smt-solving-for-bit-vectors-and-the-extensional-theory-/"
}

@inproceedings{bromberger2019spass,
    author = "Bromberger, Martin and Fleury, Mathias and Schwarz, Simon and Weidenbach, Christoph",
    title = "{SPASS-SATT}: A {CDCL(LA)} Solver",
    booktitle = "Automated Deduction -- CADE 27",
    year = "2019",
    pages = "111--122",
    doi = "10.1007/978-3-030-29436-6_7"
}

@techreport{dutertre2006simplexreport,
    author = "Dutertre, Bruno and de Moura, Leonardo",
    title = "Integrating Simplex with {DPLL(T)}",
    institution = "SRI International",
    number = "SRI-CSL-06-01",
    year = "2006",
    url = "https://yices.csl.sri.com/papers/sri-csl-06-01.pdf"
}

@misc{dutertre2006simplexslides,
    author = "Dutertre, Bruno and de Moura, Leonardo",
    title = "A Fast Linear-Arithmetic Solver for {DPLL(T)}",
    year = "2006",
    howpublished = "CAV presentation slides",
    url = "https://yices.csl.sri.com/old/slides-cav06.pdf"
}

@techreport{dutertre2006yices,
    author = "Dutertre, Bruno and de Moura, Leonardo",
    title = "The {Yices SMT} Solver",
    institution = "SRI International",
    year = "2006",
    url = "https://yices.csl.sri.com/papers/tool-paper.pdf"
}

@misc{dutertre2016yices,
    author = "Dutertre, Bruno",
    title = "The Nuts and Bolts of {Yices}",
    year = "2016",
    howpublished = "SMT Workshop, Coimbra, presentation slides",
    url = "https://yices.csl.sri.com/papers/smt2016-talk.pdf"
}

@inproceedings{lu2026selection,
    author = "Lu, Zhengyang and Sarnighausen-Cahn, Paul and Chen, Jiahao and Gurfinkel, Arie and Manea, Florin and Ganesh, Vijay",
    title = "Learning {SMT} Algorithm Selection with High-Level Natural-Language Descriptions",
    booktitle = "Foundations of Information and Knowledge Systems",
    year = "2026",
    pages = "353--358",
    doi = "10.1007/978-3-032-21540-6_23"
}

@techreport{achterberg2011rounding,
    author = "Achterberg, Tobias and Berthold, Timo and Hendel, Gregor",
    title = "Rounding and Propagation Heuristics for Mixed Integer Programming",
    institution = "Zuse Institute Berlin",
    number = "11-29",
    year = "2011",
    url = "https://edocs.tib.eu/files/e01fn13/733448909l.pdf"
}

@article{fischetti2005pump,
    author = "Fischetti, Matteo and Glover, Fred and Lodi, Andrea",
    title = "The feasibility pump",
    journal = "Mathematical Programming",
    volume = "104",
    pages = "91--104",
    year = "2005",
    doi = "10.1007/s10107-004-0570-3"
}

@phdthesis{berthold2014thesis,
    author = "Berthold, Timo",
    title = "Heuristic algorithms in global {MINLP} solvers",
    school = "Technische Universität Berlin",
    year = "2014",
    url = "https://www.zib.de/userpage/berthold/Berthold2014.pdf"
}

@article{berthold2014rens,
    author = "Berthold, Timo",
    title = "{RENS}: the optimal rounding",
    journal = "Mathematical Programming Computation",
    volume = "6",
    pages = "33--54",
    year = "2014",
    doi = "10.1007/s12532-013-0060-9"
}

@article{pugh1992omega,
    author = "Pugh, William",
    title = "The {Omega} test: a fast and practical integer programming algorithm for dependence analysis",
    journal = "Communications of the ACM",
    volume = "35",
    number = "8",
    pages = "102--114",
    year = "1992",
    url = "https://www.cs.umd.edu/~pugh/papers/omega.pdf"
}

@article{nieuwenhuis2007,
    author = "Nieuwenhuis, Robert and Oliveras, Albert",
    title = "Fast Congruence Closure and Extensions",
    journal = "Information and Computation",
    volume = "205",
    number = "4",
    pages = "557--580",
    year = "2007",
    doi = "10.1016/j.ic.2006.08.009"
}

@inproceedings{reynolds2018enumerative,
    author = "Reynolds, Andrew and Barbosa, Haniel and Fontaine, Pascal",
    title = "Revisiting Enumerative Instantiation",
    booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",
    series = "Lecture Notes in Computer Science",
    volume = "10806",
    pages = "112--131",
    publisher = "Springer",
    year = "2018",
    doi = "10.1007/978-3-319-89963-3_7",
    url = "https://hanielbarbosa.com/papers/tacas2018.pdf"
}

@inproceedings{ge2009complete,
    author = "Ge, Yeting and de Moura, Leonardo",
    title = "Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories",
    booktitle = "Computer Aided Verification",
    series = "Lecture Notes in Computer Science",
    volume = "5643",
    pages = "306--320",
    publisher = "Springer",
    year = "2009",
    doi = "10.1007/978-3-642-02658-4_25",
    url = "https://leodemoura.github.io/files/ci.pdf"
}

@manual{smtlib2026,
  author = {Barrett, Clark and Fontaine, Pascal and Tinelli, Cesare},
  title = {The {SMT-LIB} Standard: Version 2.7},
  year = {2026},
  note = {Release March 27, 2026},
  url = {https://smt-lib.org/papers/smt-lib-reference-v2.7-r2026-03-27.pdf}
}

@inproceedings{cimatti2013mathsat,
  author = {Cimatti, Alessandro and Griggio, Alberto and Schaafsma, Bastiaan Joost and Sebastiani, Roberto},
  title = {The {MathSAT5} {SMT} Solver},
  booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
  year = {2013},
  pages = {93--107},
  doi = {10.1007/978-3-642-36742-7_7},
  url = {https://es-static.fbk.eu/people/griggio/papers/tacas13.pdf}
}

@inproceedings{bjorner2023incremental,
  author = {Bj{\o}rner, Nikolaj and Fazekas, Katalin},
  title = {Incremental Pre-processing for {SMT}},
  booktitle = {Automated Deduction -- CADE 29},
  year = {2023},
  url = {https://kfazekas.github.io/papers/BjornerFazekas-CADE23.pdf}
}

@article{dillig2011cuts,
    author = {Dillig, Isil and Dillig, Thomas and Aiken, Alex},
    title = {Cuts from proofs: a complete and practical technique for solving linear inequalities over integers},
    journal = {Formal Methods in System Design},
    volume = {39},
    pages = {246--260},
    year = {2011},
    doi = {10.1007/s10703-011-0127-z},
    url = {https://doi.org/10.1007/s10703-011-0127-z}
}