{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:15Z","timestamp":1784837775050,"version":"3.55.0"},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031107689","type":"print"},{"value":"9783031107696","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The  SMT solver solves quantifier-free nonlinear real arithmetic problems by combining the cylindrical algebraic coverings method with incremental linearization in an abstraction-refinement loop. The result is a complete algebraic decision procedure that leverages efficient heuristics for refining candidate models. Furthermore, it can be used with quantifiers, integer variables, and in combination with other theories. We describe the overall framework, individual solving techniques, and a number of implementation details. We demonstrate its effectiveness with an evaluation on the SMT-LIB benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_7","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"95-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Cooperating Techniques for Solving Nonlinear Real Arithmetic in the cvc5 SMT Solver (System Description)"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0393-5739","authenticated-orcid":false,"given":"Gereon","family":"Kremer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"key":"7_CR1","unstructured":"Abbott, J., Bigatti, A.M., Palezzato, E.: New in CoCoA-5.2.4 and CoCoALib-0.99600 for SC-square. In: Satisfiability Checking and Symbolic Computation. CEUR Workshop Proceedings, vol. 2189, pp. 88\u201394. CEUR-WS.org (2018). http:\/\/ceur-ws.org\/Vol-2189\/paper4.pdf"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-319-47677-3_15","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"E \u00c1brah\u00e1m","year":"2016","unstructured":"\u00c1brah\u00e1m, E., Corzilius, F., Johnsen, E.B., Kremer, G., Mauro, J.: Zephyrus2: on the fly deployment optimization using SMT and CP technologies. In: Fr\u00e4nzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 229\u2013245. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47677-3_15"},{"key":"7_CR3","doi-asserted-by":"publisher","unstructured":"\u00c1brah\u00e1m, E., Davenport, J.H., England, M., Kremer, G.: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings. J. Logic. Algebr. Methods Program. 119(100633) (2021). https:\/\/doi.org\/10.1016\/j.jlamp.2020.100633","DOI":"10.1016\/j.jlamp.2020.100633"},{"key":"7_CR4","unstructured":"Abrah\u00e1m, E., Davenport, J.H., England, M., Kremer, G.: Proving UNSAT in SMT: the case of quantifier free non-linear real arithmetic. arXiv preprint arXiv:2108.05320 (2021)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Arnett, T.J., Cook, B., Clark, M., Rattan, K.: Fuzzy logic controller stability analysis using a satisfiability modulo theories approach. In: 19th AIAA Non-Deterministic Approaches Conference, p. 1773 (2017)","DOI":"10.2514\/6.2017-1773"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1145\/235809.235813","volume":"43","author":"S Basu","year":"1996","unstructured":"Basu, S., Pollack, R., Roy, M.F.: On the combinatorial and algebraic complexity of quantifier elimination. J. ACM 43, 1002\u20131045 (1996). https:\/\/doi.org\/10.1145\/235809.235813","journal-title":"J. ACM"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"7_CR8","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1613\/jair.1.11751","volume":"67","author":"M Cashmore","year":"2020","unstructured":"Cashmore, M., Magazzeni, D., Zehtabi, P.: Planning for hybrid systems via satisfiability modulo theories. J. Artif. Intell. Res. 67, 235\u2013283 (2020). https:\/\/doi.org\/10.1613\/jair.1.11751","journal-title":"J. Artif. Intell. Res."},{"key":"7_CR9","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Logic 19, 19:1\u201319:52 (2018). https:\/\/doi.org\/10.1145\/3230639","DOI":"10.1145\/3230639"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"GE Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134\u2013183. Springer, Heidelberg (1975). https:\/\/doi.org\/10.1007\/3-540-07407-4_17"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-642-22953-4_31","volume-title":"Fundamentals of Computation Theory","author":"F Corzilius","year":"2011","unstructured":"Corzilius, F., \u00c1brah\u00e1m, E.: Virtual substitution for SMT-solving. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol. 6914, pp. 360\u2013371. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22953-4_31"},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/978-3-319-24318-4_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2015","author":"F Corzilius","year":"2015","unstructured":"Corzilius, F., Kremer, G., Junges, S., Schupp, S., \u00c1brah\u00e1m, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360\u2013368. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24318-4_26"},{"key":"7_CR14","unstructured":"Davenport, J., England, M., Kremer, G., Tonks, Z., et al.: New opportunities for the formal proof of computational real geometry? arXiv preprint arXiv:2004.04034 (2020)"},{"issue":"1","key":"7_CR15","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1), 29\u201335 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80004-X","journal-title":"J. Symb. Comput."},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"2","key":"7_CR17","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. ACM SIGSAM Bull. 31(2), 2\u20139 (1997). https:\/\/doi.org\/10.1145\/261320.261324","journal-title":"ACM SIGSAM Bull."},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-31612-8_14","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"S Ermon","year":"2012","unstructured":"Ermon, S., Le Bras, R., Gomes, C.P., Selman, B., van Dover, R.B.: SMT-aided combinatorial materials discovery. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 172\u2013185. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31612-8_14"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"900","DOI":"10.1007\/978-3-642-33558-7_64","volume-title":"Principles and Practice of Constraint Programming","author":"R Fagerberg","year":"2012","unstructured":"Fagerberg, R., Flamm, C., Merkle, D., Peters, P.: Exploring chemistry using SMT. In: Milano, M. (ed.) CP 2012. LNCS, pp. 900\u2013915. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33558-7_64"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-79719-7_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"G Faure","year":"2008","unstructured":"Faure, G., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: SAT modulo the theory of linear arithmetic: exact, inexact and commercial solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 77\u201390. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-79719-7_8"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-319-66167-4_11","volume-title":"Frontiers of Combining Systems","author":"P Fontaine","year":"2017","unstructured":"Fontaine, P., Ogawa, M., Sturm, T., Vu, X.T.: Subtropical satisfiability. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 189\u2013206. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_11"},{"key":"7_CR23","unstructured":"Fontaine, P., Ogawa, M., Sturm, T., Vu, X.T., et al.: Wrapping computer algebra is surprisingly successful for non-linear SMT. In: SC-square 2018-Third International Workshop on Satisfiability Checking and Symbolic Computation (2018)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_14"},{"key":"7_CR25","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/S0747-7171(88)80005-1","volume":"5","author":"DY Grigor\u2019ev","year":"1988","unstructured":"Grigor\u2019ev, D.Y., Vorobjov, N.: Solving systems of polynomial inequalities in subexponential time. J. Symb. Comput. 5, 37\u201364 (1988). https:\/\/doi.org\/10.1016\/S0747-7171(88)80005-1","journal-title":"J. Symb. Comput."},{"key":"7_CR26","doi-asserted-by":"publisher","unstructured":"Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: International Symposium on Symbolic and Algebraic Computation, pp. 261\u2013264 (1990). https:\/\/doi.org\/10.1145\/96877.96943","DOI":"10.1145\/96877.96943"},{"key":"7_CR27","unstructured":"Hong, H.: Comparison of several decision algorithms for the existential theory of the reals. RES report, Johannes Kepler University (1991)"},{"key":"7_CR28","doi-asserted-by":"publisher","unstructured":"Jovanovi\u0107, D., Barrett, C., de Moura, L.: The design and implementation of the model constructing satisfiability calculus. In: Formal Methods in Computer-Aided Design, pp. 173\u2013180. IEEE (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.7027033","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"7_CR29","unstructured":"Jovanovic, D., Dutertre, B.: LibPoly: a library for reasoning about polynomials. In: Satisfiability Modulo Theories. CEUR Workshop Proceedings, vol. 1889. CEUR-WS.org (2017). http:\/\/ceur-ws.org\/Vol-1889\/paper3.pdf"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-31365-3_27","volume-title":"Automated Reasoning","author":"D Jovanovi\u0107","year":"2012","unstructured":"Jovanovi\u0107, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339\u2013354. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_27"},{"key":"7_CR31","unstructured":"Ko\u0161ta, M., Sturm, T.: A generalized framework for virtual substitution. CoRR abs\/1501.05826 (2015)"},{"key":"7_CR32","doi-asserted-by":"publisher","unstructured":"Kremer, G.: Cylindrical algebraic decomposition for nonlinear arithmetic problems. Ph.D. thesis, RWTH Aachen University (2020). https:\/\/doi.org\/10.18154\/RWTH-2020-05913","DOI":"10.18154\/RWTH-2020-05913"},{"key":"7_CR33","doi-asserted-by":"publisher","unstructured":"Kremer, G., Brandt, J.: Implementing arithmetic over algebraic numbers: a tutorial for Lazard\u2019s lifting scheme in CAD. In: Symbolic and Numeric Algorithms for Scientific Computing, pp. 4\u201310 (2021). https:\/\/doi.org\/10.1109\/SYNASC54541.2021.00013","DOI":"10.1109\/SYNASC54541.2021.00013"},{"key":"7_CR34","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/j.jsc.2019.07.018","volume":"100","author":"G Kremer","year":"2020","unstructured":"Kremer, G., \u00c1brah\u00e1m, E.: Fully incremental cylindrical algebraic decomposition. J. Symb. Comput. 100, 11\u201337 (2020). https:\/\/doi.org\/10.1016\/j.jsc.2019.07.018","journal-title":"J. Symb. Comput."},{"key":"7_CR35","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-1-4612-2628-4_29","volume-title":"Algebraic Geometry and Its Applications","author":"D Lazard","year":"1994","unstructured":"Lazard, D.: An improved projection for cylindrical algebraic decomposition. In: Bajaj, C.L. (ed.) Algebraic Geometry and Its Applications, pp. 467\u2013476. Springer, New York (1994). https:\/\/doi.org\/10.1007\/978-1-4612-2628-4_29"},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-38574-2_13","volume-title":"Automated Deduction \u2013 CADE-24","author":"U Loup","year":"2013","unstructured":"Loup, U., Scheibler, K., Corzilius, F., \u00c1brah\u00e1m, E., Becker, B.: A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 193\u2013207. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_13"},{"key":"7_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-15984-3_277","volume-title":"EUROCAL \u201985","author":"S McCallum","year":"1985","unstructured":"McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B.F. (ed.) EUROCAL 1985. LNCS, vol. 204, pp. 277\u2013278. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15984-3_277"},{"key":"7_CR38","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.jsc.2017.12.002","volume":"92","author":"S McCallum","year":"2019","unstructured":"McCallum, S., Parusi\u0144ski, A., Paunescu, L.: Validity proof of Lazard\u2019s method for cad construction. J. Symb. Comput. 92, 52\u201369 (2019). https:\/\/doi.org\/10.1016\/j.jsc.2017.12.002","journal-title":"J. Symb. Comput."},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L de Moura","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_1"},{"issue":"6","key":"7_CR40","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","journal-title":"J. ACM"},{"key":"7_CR41","doi-asserted-by":"publisher","unstructured":"Renegar, J.: A faster PSPACE algorithm for deciding the existential theory of the reals. In: Symposium on Foundations of Computer Science, pp. 291\u2013295 (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21945","DOI":"10.1109\/SFCS.1988.21945"},{"key":"7_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-66167-4_2","volume-title":"Frontiers of Combining Systems","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Tinelli, C., Jovanovi\u0107, D., Barrett, C.: Designing theory solvers with extensions. In: Dixon, C., Finger, M. (eds.) FroCoS 2017. LNCS (LNAI), vol. 10483, pp. 22\u201340. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_2"},{"key":"7_CR43","doi-asserted-by":"publisher","unstructured":"Roselli, S.F., Bengtsson, K., \u00c5kesson, K.: SMT solvers for job-shop scheduling problems: models comparison and performance evaluation. In: International Conference on Automation Science and Engineering (CASE), pp. 547\u2013552 (2018). https:\/\/doi.org\/10.1109\/COASE.2018.8560344","DOI":"10.1109\/COASE.2018.8560344"},{"key":"7_CR44","unstructured":"SMT-COMP 2021 (2021). https:\/\/smt-comp.github.io\/2021\/"},{"key":"7_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40229-1_16","volume-title":"Automated Reasoning","author":"VX Tung","year":"2016","unstructured":"Tung, V.X., Van Khanh, T., Ogawa, M.: raSAT: an SMT solver for polynomial constraints. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 228\u2013237. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_16"},{"issue":"2","key":"7_CR46","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra-the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85\u2013101 (1997). https:\/\/doi.org\/10.1007\/s002000050055","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"7_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/978-3-030-94583-1_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Y Zohar","year":"2022","unstructured":"Zohar, Y., et al.: Bit-precise reasoning via Int-blasting. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 496\u2013518. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_24"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:12:53Z","timestamp":1659316373000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}