36:
1713:
Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022).
457:
Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark (2022).
789:
Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). "Invertibility
Conditions for Floating-Point Formulas". In Dillig, Isil; Tasiran, Serdar (eds.).
899:
Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (2023-09-15).
54:
1803:
232:(SMT) solvers. The latest major versions of CVC are CVC4 and CVC5 (stylized cvc5); earlier versions include CVC, CVC Lite, and CVC3. Both CVC4 and cvc5 support the
1456:
Backes, John; Bolignano, Pauline; Cook, Byron; Dodge, Catherine; Gacek, Andrew; Luckow, Kasper; Rungta, Neha; Tkachuk, Oksana; Varming, Carsten (October 2018).
248:. Both CVC4 and cvc5 can output proofs that can be independently checked in the LFSC format, cvc5 additionally supports the Alethe and Lean 4 formats. cvc5 has
1113:
Reynolds, Andrew; Barbosa, Haniel; Larraz, Daniel; Tinelli, Cesare (2020-05-30). "Scalable
Algorithms for Abduction via Enumerative Syntax-Guided Synthesis".
423:
Barrett, Clark; Tinelli, Cesare (2018), Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), "Satisfiability Modulo
Theories",
1798:
237:
1808:
1407:
Companion
Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity
1753:
Barrett, Clark; Conway, Christopher L.; Deters, Morgan; Hadarean, Liana; Jovanović, Dejan; King, Tim; Reynolds, Andrew; Tinelli, Cesare (2011).
1793:
1774:
1735:
1698:
1571:
1520:
1475:
1432:
1350:
1311:
1270:
1231:
1192:
1130:
1089:
1044:
1004:
967:
883:
846:
809:
773:
736:
479:
442:
72:
271:
in the years 2014-2020, and cvc5 has competed in the years 2021-2022. CVC4 competed in SyGuS-COMP in the years 2015-2019, and in
365:
268:
229:
257:
660:
Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: Results and
Analysis".
613:
Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-11-22). "SyGuS-Comp 2016: Results and
Analysis".
566:
Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "Results and
Analysis of SyGuS-Comp'15".
1597:
Barbosa, Haniel; Keller, Chantal; Reynolds, Andrew; Viswanathan, Arjun; Tinelli, Cesare; Barrett, Clark (2023-06-03).
272:
261:
129:
1547:
Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017).
379:
1722:. Lecture Notes in Computer Science. Vol. 13243. Cham: Springer International Publishing. pp. 415–442.
1558:. Lecture Notes in Computer Science. Vol. 10427. Cham: Springer International Publishing. pp. 126–133.
991:. Lecture Notes in Computer Science. Vol. 10395. Cham: Springer International Publishing. pp. 148–165.
295:
291:
180:
1257:. Lecture Notes in Computer Science. Vol. 13372. Cham: Springer International Publishing. pp. 92–106.
1031:. Lecture Notes in Computer Science. Vol. 9938. Cham: Springer International Publishing. pp. 244–261.
870:. Lecture Notes in Computer Science. Vol. 9195. Cham: Springer International Publishing. pp. 197–213.
833:. Lecture Notes in Computer Science. Vol. 9322. Cham: Springer International Publishing. pp. 135–150.
760:. Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 680–695.
723:. Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 646–662.
466:. Lecture Notes in Computer Science. Vol. 13385. Cham: Springer International Publishing. pp. 15–35.
1507:. Lecture Notes in Computer Science. Vol. 13371. Cham: Springer International Publishing. pp. 3–18.
954:. Lecture Notes in Computer Science. Vol. 9706. Cham: Springer International Publishing. pp. 82–98.
1076:. Lecture Notes in Computer Science. Vol. 13965. Cham: Springer Nature Switzerland. pp. 163–186.
323:
315:
1761:. Lecture Notes in Computer Science. Vol. 6806. Berlin, Heidelberg: Springer. pp. 171–177.
1685:. Lecture Notes in Computer Science. Vol. 8413. Berlin, Heidelberg: Springer. pp. 389–391.
1375:
1021:
371:
334:
175:
96:
1754:
1741:
1715:
1678:
1659:
1620:
1577:
1526:
1481:
1438:
1410:
1409:. SPLASH Companion 2021. New York, NY, USA: Association for Computing Machinery. pp. 19–21.
1356:
1317:
1276:
1237:
1198:
1095:
1050:
984:
928:
863:
753:
716:
695:
669:
648:
622:
601:
575:
485:
221:
100:
1500:
1250:
1069:
947:
826:
794:. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 116–136.
459:
1212:"Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs"
1770:
1731:
1694:
1567:
1548:
1516:
1471:
1428:
1346:
1307:
1266:
1227:
1188:
1126:
1085:
1040:
1000:
963:
920:
879:
842:
825:
Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015).
805:
769:
732:
687:
640:
593:
475:
438:
311:
245:
160:
1762:
1723:
1686:
1649:
1610:
1559:
1508:
1463:
1420:
1381:
1338:
1299:
1258:
1219:
1180:
1136:
1118:
1077:
1032:
992:
955:
912:
871:
834:
795:
761:
752:
Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014).
724:
679:
632:
585:
467:
428:
319:
249:
217:
187:
155:
1210:
Sun, Maolin; Yang, Yibiao; Wen, Ming; Wang, Yongcong; Zhou, Yuming; Jin, Hai (2023-07-26).
1177:
Proceedings of the 37th IEEE/ACM International
Conference on Automated Software Engineering
827:"A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings"
283:
715:
Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014).
370:
CVC4 has been applied to the synthesis of recursive programs. and to the verification of
382:. CVC4 is one of the back-end reasoners supported by CBMC, the C Bounded Model Checker.
1141:
399:
375:
1329:
Sun, Maolin; Yang, Yibiao; Wang, Yang; Wen, Ming; Jia, Haoxiang; Zhou, Yuming (2023).
1787:
1745:
1663:
1624:
1581:
1530:
1442:
1360:
1321:
1280:
1241:
1202:
1099:
932:
489:
307:
1640:
Desharnais, Martin; Vukmirović, Petar; Blanchette, Jasmin; Wenzel, Makarius (2022).
1485:
699:
540:
516:
1335:
2023 38th IEEE/ACM International
Conference on Automated Software Engineering (ASE)
1054:
605:
327:
192:
1179:. ASE '22. New York, NY, USA: Association for Computing Machinery. pp. 1–10.
652:
1766:
1727:
1690:
1403:"Programming-by-example by programming-by-example: Synthesis of looping programs"
1303:
1223:
1036:
996:
875:
765:
728:
433:
1598:
1563:
1512:
1467:
1342:
1330:
1262:
1122:
1081:
959:
838:
800:
471:
342:
1457:
1289:
1211:
916:
1654:
1641:
91:
1385:
948:"A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT"
924:
900:
691:
644:
597:
1424:
1298:. ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 2224–2236.
1290:"Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations"
1184:
299:
946:
Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2016).
1402:
1295:
2023 IEEE/ACM 45th
International Conference on Software Engineering (ICSE)
1216:
2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)
1172:
717:"A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions"
636:
303:
241:
1218:. ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 69–81.
1117:. Lecture Notes in Computer Science. Vol. 12166. pp. 141–160.
983:
Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017).
683:
589:
1068:
Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023).
287:
279:
233:
1331:"SMT Solver Validation Empowered by Large Pre-Trained Language Models"
901:"Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences"
1459:
Semantic-based Automated Reasoning for AWS Access Policies using SMT
1293:
1251:"Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers"
17:
1415:
1020:
Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016).
674:
627:
580:
253:
148:
1615:
282:
architecture, and supports the theories of linear arithmetic over
168:
164:
1720:
Tools and Algorithms for the Construction and Analysis of Systems
1683:
Tools and Algorithms for the Construction and Analysis of Systems
1377:
Fuzz-testing SMT Solvers with Formula Weakening and Strengthening
754:"A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors"
462:. In Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.).
460:"Flexible Proof Production in an Industrial-Strength SMT Solver"
1171:
Bringolf, Mauro; Winterer, Dominik; Su, Zhendong (2023-01-05).
1173:"Finding and Understanding Incompleteness Bugs in SMT Solvers"
29:
427:, Cham: Springer International Publishing, pp. 305–343,
356:
cvc5 has been subject to several independent test campaigns.
333:
In addition to standard SMT and SyGuS solving, cvc5 supports
1599:"An Interactive SMT Tactic in Coq using Abductive Reasoning"
203:
1589:
1156:
503:
374:
access policies. CVC4 and cvc5 have been integrated with
1549:"SMTCoq: A Plug-In for Integrating SMT Solvers into Coq"
1249:
Niemetz, Aina; Preiner, Mathias; Barrett, Clark (2022).
1027:. In Artho, Cyrille; Legay, Axel; Peled, Doron (eds.).
864:"A Decision Procedure for (Co)datatypes in SMT Solvers"
862:
Reynolds, Andrew; Blanchette, Jasmin Christian (2015).
50:
1716:"Cvc5: A Versatile and Industrial-Strength SMT Solver"
662:
Electronic Proceedings in Theoretical Computer Science
615:
Electronic Proceedings in Theoretical Computer Science
568:
Electronic Proceedings in Theoretical Computer Science
1648:. Schloss-Dagstuhl - Leibniz Zentrum für Informatik.
1288:
Kim, Jongwook; So, Sunbeom; Oh, Hakjoo (2023-07-26).
198:
186:
174:
154:
144:
128:
106:
90:
45:
may be too technical for most readers to understand
1757:. In Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.).
1029:Automated Technology for Verification and Analysis
1022:"A Decision Procedure for Separation Logic in SMT"
366:Satisfiability modulo theories § Applications
337:, which is the problem of constructing a formula
240:input formats for solving SMT problems, and the
1646:DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8
1677:Kroening, Daniel; Tautschnig, Michael (2014).
950:. In Olivetti, Nicola; Tiwari, Ashish (eds.).
1681:. In Ábrahám, Erika; Havelund, Klaus (eds.).
1554:. In Majumdar, Rupak; Kunčak, Viktor (eds.).
1501:"A Billion SMT Queries a Day (Invited Paper)"
866:. In Felty, Amy P.; Middeldorp, Aart (eds.).
8:
85:
829:. In Lutz, Carsten; Ranise, Silvio (eds.).
756:. In Biere, Armin; Bloem, Roderick (eds.).
719:. In Biere, Armin; Bloem, Roderick (eds.).
1503:. In Shoham, Sharon; Vizel, Yakir (eds.).
1253:. In Shoham, Sharon; Vizel, Yakir (eds.).
1072:. In Enea, Constantin; Lal, Akash (eds.).
84:
1718:. In Fisman, Dana; Rosu, Grigore (eds.).
1653:
1614:
1414:
1140:
799:
673:
626:
579:
432:
326:among others. cvc5 additionally supports
73:Learn how and when to remove this message
57:, without removing the technical details.
391:
1804:Satisfiability modulo theories solvers
985:"Relational Constraint Solving in SMT"
1070:"Satisfiability Modulo Finite Fields"
55:make it understandable to non-experts
7:
1642:"Seventeen Provers Under the Hammer"
1380:(Master Thesis thesis). ETH Zurich.
25:
1679:"CBMC – C Bounded Model Checker"
400:"Release cvc5-1.0.8 · cvc5/cvc5"
34:
1799:Free software programmed in C++
987:. In de Moura, Leonardo (ed.).
1809:Software using the BSD license
905:Journal of Automated Reasoning
831:Frontiers of Combining Systems
230:satisfiability modulo theories
1:
1794:Free and open-source software
1401:Berman, Shmuel (2021-10-17).
989:Automated Deduction – CADE 26
868:Automated Deduction - CADE-25
1767:10.1007/978-3-642-22110-1_14
1728:10.1007/978-3-030-99524-9_24
1691:10.1007/978-3-642-54862-8_26
1304:10.1109/ICSE48619.2023.00187
1224:10.1109/ICSE48619.2023.00018
1037:10.1007/978-3-319-46520-3_16
997:10.1007/978-3-319-63046-5_10
876:10.1007/978-3-319-21401-6_13
766:10.1007/978-3-319-08867-9_45
729:10.1007/978-3-319-08867-9_43
434:10.1007/978-3-319-10575-8_11
226:Cooperating Validity Checker
1759:Computer Aided Verification
1564:10.1007/978-3-319-63390-9_7
1556:Computer Aided Verification
1513:10.1007/978-3-031-13185-1_1
1505:Computer Aided Verification
1468:10.23919/FMCAD.2018.8602994
1343:10.1109/ase56229.2023.00180
1263:10.1007/978-3-031-13188-2_5
1255:Computer Aided Verification
1123:10.1007/978-3-030-51074-9_9
1082:10.1007/978-3-031-37703-7_8
1074:Computer Aided Verification
960:10.1007/978-3-319-40229-1_7
839:10.1007/978-3-319-24246-0_9
801:10.1007/978-3-030-25543-5_8
792:Computer Aided Verification
758:Computer Aided Verification
721:Computer Aided Verification
472:10.1007/978-3-031-10769-6_3
1825:
917:10.1007/s10817-023-09682-2
425:Handbook of Model Checking
363:
290:, fixed-width bitvectors,
112:; 2 years ago
1655:10.4230/LIPIcs.ITP.2022.8
292:floating-point arithmetic
140:
135:1.0.8 / 31 August 2023
124:
1603:EPiC Series in Computing
1386:10.3929/ethz-b-000507582
1374:Bringolf, Mauro (2021).
349:to prove a goal formula
1425:10.1145/3484271.3484977
1185:10.1145/3551349.3560435
324:uninterpreted functions
1462:. IEEE. pp. 1–9.
1337:. pp. 1288–1300.
1499:Rungta, Neha (2022).
228:(CVC) is a family of
1609:. EasyChair: 11–22.
637:10.4204/EPTCS.229.13
1590:Barbosa et al. 2022
1157:Barbosa et al. 2022
1115:Automated Reasoning
952:Automated Reasoning
684:10.4204/EPTCS.260.9
590:10.4204/EPTCS.202.3
504:Barbosa et al. 2022
464:Automated Reasoning
372:Amazon Web Services
335:abductive reasoning
97:Stanford University
87:
222:mathematical logic
101:University of Iowa
1776:978-3-642-22110-1
1737:978-3-030-99524-9
1700:978-3-642-54862-8
1573:978-3-319-63390-9
1522:978-3-031-13185-1
1477:978-0-9835678-8-2
1434:978-1-4503-9088-0
1352:979-8-3503-2996-4
1313:978-1-6654-5701-9
1272:978-3-031-13188-2
1233:978-1-6654-5701-9
1194:978-1-4503-9475-8
1132:978-3-030-51073-2
1091:978-3-031-37703-7
1046:978-3-319-46520-3
1006:978-3-319-63046-5
969:978-3-319-40229-1
885:978-3-319-21401-6
848:978-3-319-24246-0
811:978-3-030-25543-5
775:978-3-319-08867-9
738:978-3-319-08867-9
481:978-3-031-10769-6
444:978-3-319-10575-8
267:CVC4 competed in
246:program synthesis
214:
213:
83:
82:
75:
16:(Redirected from
1816:
1780:
1749:
1705:
1704:
1674:
1668:
1667:
1657:
1637:
1631:
1628:
1618:
1585:
1553:
1541:
1535:
1534:
1496:
1490:
1489:
1453:
1447:
1446:
1418:
1398:
1392:
1389:
1370:
1368:
1367:
1325:
1284:
1245:
1206:
1166:
1160:
1153:
1147:
1146:
1144:
1110:
1104:
1103:
1065:
1059:
1058:
1026:
1017:
1011:
1010:
980:
974:
973:
943:
937:
936:
896:
890:
889:
859:
853:
852:
822:
816:
815:
803:
786:
780:
779:
749:
743:
742:
712:
706:
703:
677:
656:
630:
609:
583:
561:
555:
554:
552:
551:
537:
531:
530:
528:
527:
513:
507:
500:
494:
493:
454:
448:
447:
436:
420:
414:
413:
411:
410:
396:
352:
348:
340:
320:separation logic
218:computer science
210:
207:
205:
156:Operating system
120:
118:
113:
88:
78:
71:
67:
64:
58:
38:
37:
30:
21:
1824:
1823:
1819:
1818:
1817:
1815:
1814:
1813:
1784:
1783:
1777:
1752:
1738:
1712:
1709:
1708:
1701:
1676:
1675:
1671:
1639:
1638:
1634:
1596:
1574:
1551:
1546:
1542:
1538:
1523:
1498:
1497:
1493:
1478:
1455:
1454:
1450:
1435:
1400:
1399:
1395:
1373:
1365:
1363:
1353:
1328:
1314:
1287:
1273:
1248:
1234:
1209:
1195:
1170:
1167:
1163:
1154:
1150:
1133:
1112:
1111:
1107:
1092:
1067:
1066:
1062:
1047:
1024:
1019:
1018:
1014:
1007:
982:
981:
977:
970:
945:
944:
940:
898:
897:
893:
886:
861:
860:
856:
849:
824:
823:
819:
812:
788:
787:
783:
776:
751:
750:
746:
739:
714:
713:
709:
659:
612:
565:
562:
558:
549:
547:
539:
538:
534:
525:
523:
515:
514:
510:
501:
497:
482:
456:
455:
451:
445:
422:
421:
417:
408:
406:
398:
397:
393:
388:
368:
362:
350:
346:
345:with a formula
338:
306:(used to model
202:
136:
116:
114:
111:
107:Initial release
79:
68:
62:
59:
51:help improve it
48:
39:
35:
28:
23:
22:
15:
12:
11:
5:
1822:
1820:
1812:
1811:
1806:
1801:
1796:
1786:
1785:
1782:
1781:
1775:
1750:
1736:
1707:
1706:
1699:
1669:
1632:
1630:
1629:
1593:
1592:, p. 425)
1586:
1572:
1536:
1521:
1491:
1476:
1448:
1433:
1393:
1391:
1390:
1371:
1351:
1326:
1312:
1285:
1271:
1246:
1232:
1207:
1193:
1161:
1159:, p. 426)
1148:
1131:
1105:
1090:
1060:
1045:
1012:
1005:
975:
968:
938:
891:
884:
854:
847:
817:
810:
781:
774:
744:
737:
707:
705:
704:
657:
610:
556:
532:
517:"Participants"
508:
506:, p. 417)
495:
480:
449:
443:
415:
390:
389:
387:
384:
361:
358:
308:dynamic arrays
300:(co)-datatypes
278:CVC4 uses the
275:in 2013-2015.
212:
211:
200:
196:
195:
190:
184:
183:
181:Theorem prover
178:
172:
171:
158:
152:
151:
146:
142:
141:
138:
137:
134:
132:
130:Stable release
126:
125:
122:
121:
108:
104:
103:
94:
81:
80:
42:
40:
33:
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
1821:
1810:
1807:
1805:
1802:
1800:
1797:
1795:
1792:
1791:
1789:
1778:
1772:
1768:
1764:
1760:
1756:
1751:
1747:
1743:
1739:
1733:
1729:
1725:
1721:
1717:
1711:
1710:
1702:
1696:
1692:
1688:
1684:
1680:
1673:
1670:
1665:
1661:
1656:
1651:
1647:
1643:
1636:
1633:
1626:
1622:
1617:
1616:10.29007/432m
1612:
1608:
1604:
1600:
1594:
1591:
1587:
1583:
1579:
1575:
1569:
1565:
1561:
1557:
1550:
1544:
1543:
1540:
1537:
1532:
1528:
1524:
1518:
1514:
1510:
1506:
1502:
1495:
1492:
1487:
1483:
1479:
1473:
1469:
1465:
1461:
1460:
1452:
1449:
1444:
1440:
1436:
1430:
1426:
1422:
1417:
1412:
1408:
1404:
1397:
1394:
1387:
1383:
1379:
1378:
1372:
1362:
1358:
1354:
1348:
1344:
1340:
1336:
1332:
1327:
1323:
1319:
1315:
1309:
1305:
1301:
1297:
1296:
1291:
1286:
1282:
1278:
1274:
1268:
1264:
1260:
1256:
1252:
1247:
1243:
1239:
1235:
1229:
1225:
1221:
1217:
1213:
1208:
1204:
1200:
1196:
1190:
1186:
1182:
1178:
1174:
1169:
1168:
1165:
1162:
1158:
1152:
1149:
1143:
1138:
1134:
1128:
1124:
1120:
1116:
1109:
1106:
1101:
1097:
1093:
1087:
1083:
1079:
1075:
1071:
1064:
1061:
1056:
1052:
1048:
1042:
1038:
1034:
1030:
1023:
1016:
1013:
1008:
1002:
998:
994:
990:
986:
979:
976:
971:
965:
961:
957:
953:
949:
942:
939:
934:
930:
926:
922:
918:
914:
910:
906:
902:
895:
892:
887:
881:
877:
873:
869:
865:
858:
855:
850:
844:
840:
836:
832:
828:
821:
818:
813:
807:
802:
797:
793:
785:
782:
777:
771:
767:
763:
759:
755:
748:
745:
740:
734:
730:
726:
722:
718:
711:
708:
701:
697:
693:
689:
685:
681:
676:
671:
667:
663:
658:
654:
650:
646:
642:
638:
634:
629:
624:
620:
616:
611:
607:
603:
599:
595:
591:
587:
582:
577:
573:
569:
564:
563:
560:
557:
546:
542:
536:
533:
522:
518:
512:
509:
505:
499:
496:
491:
487:
483:
477:
473:
469:
465:
461:
453:
450:
446:
440:
435:
430:
426:
419:
416:
405:
401:
395:
392:
385:
383:
381:
377:
373:
367:
359:
357:
354:
344:
336:
331:
329:
328:finite fields
325:
321:
317:
313:
309:
305:
301:
297:
293:
289:
285:
281:
276:
274:
270:
265:
263:
259:
255:
251:
247:
243:
239:
235:
231:
227:
223:
219:
209:
201:
197:
194:
191:
189:
185:
182:
179:
177:
173:
170:
166:
162:
159:
157:
153:
150:
147:
143:
139:
133:
131:
127:
123:
109:
105:
102:
98:
95:
93:
89:
77:
74:
66:
63:November 2023
56:
52:
46:
43:This article
41:
32:
31:
19:
1758:
1719:
1682:
1672:
1645:
1635:
1606:
1602:
1555:
1539:
1504:
1494:
1458:
1451:
1406:
1396:
1376:
1364:. Retrieved
1334:
1294:
1254:
1215:
1176:
1164:
1151:
1114:
1108:
1073:
1063:
1028:
1015:
988:
978:
951:
941:
908:
904:
894:
867:
857:
830:
820:
791:
784:
757:
747:
720:
710:
665:
661:
618:
614:
571:
567:
559:
548:. Retrieved
544:
535:
524:. Retrieved
520:
511:
498:
463:
452:
424:
418:
407:. Retrieved
403:
394:
369:
360:Applications
355:
341:that can be
332:
277:
266:
225:
215:
193:BSD 3-clause
92:Developer(s)
69:
60:
44:
1588:For cvc5: (
621:: 178–202.
244:format for
1788:Categories
1595:For cvc5:
1545:For CVC4:
1416:2108.08724
1366:2023-11-29
675:1711.11438
668:: 97–115.
628:1611.07627
581:1602.01170
550:2023-11-29
541:"SMT-COMP"
526:2023-11-29
409:2023-11-29
386:References
364:See also:
310:), finite
145:Written in
27:SMT solver
1746:247857361
1664:251322787
1625:259070258
1582:206701576
1531:251447649
1443:237213485
1361:265055537
1322:259860926
1281:251447764
1242:259860528
1203:255441416
1100:257235627
933:261829653
925:1573-0670
911:(3): 32.
692:2075-2180
645:2075-2180
598:2075-2180
490:250164402
343:conjoined
316:relations
304:sequences
284:rationals
1486:52237693
700:37464992
574:: 3–26.
545:SMT-COMP
521:SMT-COMP
380:Isabelle
288:integers
269:SMT-COMP
250:bindings
242:SyGuS-IF
1142:7324138
1055:6753369
606:2086015
296:strings
280:DPLL(T)
234:SMT-LIB
206:.github
199:Website
188:License
161:Windows
115: (
49:Please
1773:
1755:"CVC4"
1744:
1734:
1697:
1662:
1623:
1580:
1570:
1529:
1519:
1484:
1474:
1441:
1431:
1359:
1349:
1320:
1310:
1279:
1269:
1240:
1230:
1201:
1191:
1139:
1129:
1098:
1088:
1053:
1043:
1003:
966:
931:
923:
882:
845:
808:
772:
735:
698:
690:
653:440389
651:
643:
604:
596:
488:
478:
441:
404:GitHub
322:, and
260:, and
258:Python
1742:S2CID
1660:S2CID
1621:S2CID
1578:S2CID
1552:(PDF)
1527:S2CID
1482:S2CID
1439:S2CID
1411:arXiv
1357:S2CID
1318:S2CID
1277:S2CID
1238:S2CID
1199:S2CID
1096:S2CID
1051:S2CID
1025:(PDF)
929:S2CID
696:S2CID
670:arXiv
649:S2CID
623:arXiv
602:S2CID
576:arXiv
486:S2CID
169:macOS
165:Linux
1771:ISBN
1732:ISBN
1695:ISBN
1568:ISBN
1517:ISBN
1472:ISBN
1429:ISBN
1347:ISBN
1308:ISBN
1267:ISBN
1228:ISBN
1189:ISBN
1127:ISBN
1086:ISBN
1041:ISBN
1001:ISBN
964:ISBN
921:ISSN
880:ISBN
843:ISBN
806:ISBN
770:ISBN
733:ISBN
688:ISSN
641:ISSN
594:ISSN
476:ISBN
439:ISBN
378:and
314:and
312:sets
286:and
273:CASC
262:Java
252:for
238:TPTP
236:and
220:and
204:cvc5
176:Type
117:2022
110:2022
99:and
86:CVC5
18:CVC4
1763:doi
1724:doi
1687:doi
1650:doi
1611:doi
1560:doi
1509:doi
1464:doi
1421:doi
1382:doi
1339:doi
1300:doi
1259:doi
1220:doi
1181:doi
1137:PMC
1119:doi
1078:doi
1033:doi
993:doi
956:doi
913:doi
872:doi
835:doi
796:doi
762:doi
725:doi
680:doi
666:260
633:doi
619:229
586:doi
572:202
468:doi
429:doi
376:Coq
254:C++
216:In
208:.io
149:C++
53:to
1790::
1769:.
1740:.
1730:.
1693:.
1658:.
1644:.
1619:.
1607:94
1605:.
1601:.
1576:.
1566:.
1525:.
1515:.
1480:.
1470:.
1437:.
1427:.
1419:.
1405:.
1355:.
1345:.
1333:.
1316:.
1306:.
1292:.
1275:.
1265:.
1236:.
1226:.
1214:.
1197:.
1187:.
1175:.
1135:.
1125:.
1094:.
1084:.
1049:.
1039:.
999:.
962:.
927:.
919:.
909:67
907:.
903:.
878:.
841:.
804:.
768:.
731:.
694:.
686:.
678:.
664:.
647:.
639:.
631:.
617:.
600:.
592:.
584:.
570:.
543:.
519:.
484:.
474:.
437:,
402:.
353:.
330:.
318:,
302:,
298:,
294:,
264:.
256:,
224:,
167:,
163:,
1779:.
1765::
1748:.
1726::
1703:.
1689::
1666:.
1652::
1627:.
1613::
1584:.
1562::
1533:.
1511::
1488:.
1466::
1445:.
1423::
1413::
1388:.
1384::
1369:.
1341::
1324:.
1302::
1283:.
1261::
1244:.
1222::
1205:.
1183::
1155:(
1145:.
1121::
1102:.
1080::
1057:.
1035::
1009:.
995::
972:.
958::
935:.
915::
888:.
874::
851:.
837::
814:.
798::
778:.
764::
741:.
727::
702:.
682::
672::
655:.
635::
625::
608:.
588::
578::
553:.
529:.
502:(
492:.
470::
431::
412:.
351:C
347:A
339:B
119:)
76:)
70:(
65:)
61:(
47:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.