{"entities":{"Q7034852":{"pageid":21711996,"ns":120,"title":"Item:Q7034852","lastrevid":104086235,"modified":"2026-06-06T09:05:27Z","type":"item","id":"Q7034852","labels":{"en":{"language":"en","value":"MCSat-based finite field reasoning in the \\textsc{Yices2} SMT solver (short paper)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7977165"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$A5EFB9D8-C6CF-49A4-9563-B8F7C113CB7E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1659d6097ffe70b9ee9b9510d1b7f4851d11ea6a","datavalue":{"value":{"text":"MCSat-based finite field reasoning in the \\textsc{Yices2} SMT solver (short paper)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7034852$AA70017E-7D76-47EF-88BE-6849586E52F2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a74839b2a1d9e1a827cb577e04c5ce39cfe0d5de","datavalue":{"value":"10.1007/978-3-031-63498-7_23","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7034852$7327B516-0159-4EFC-9302-97607D9DA261","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"65b2c44308686fce031a7f4d2c9aa87d83fa4b08","datavalue":{"value":{"entity-type":"item","numeric-id":6869960,"id":"Q6869960"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$DBF15958-B09D-4898-B2F8-946C9F3D6B77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"59c49857b114968b9492d4363ca3a37d7cfd6e4a","datavalue":{"value":{"entity-type":"item","numeric-id":2110232,"id":"Q2110232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$95CD2720-FF56-42B9-A474-9B55C31754EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"637b63b8551b0d9a45289b2321fc07fbecec8861","datavalue":{"value":{"entity-type":"item","numeric-id":831940,"id":"Q831940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$0882E018-6E02-47BA-AF31-94FD4E24061F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a6be8d909a46685b6a24cecd253b3dd33cd2a6cb","datavalue":{"value":{"entity-type":"item","numeric-id":832718,"id":"Q832718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$0DF15CEB-A566-4C0C-AD43-4E498F934700","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f17059e6c6c8a57972334867cc4d511b5d1368f5","datavalue":{"value":{"entity-type":"item","numeric-id":507357,"id":"Q507357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$43520B5E-04F5-4CF7-98FD-6F5126CB77B2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"faebccf51ad7ddcce1eed4a97c7e0eb92d585316","datavalue":{"value":{"time":"+2025-01-31T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7034852$A6EEEB67-622F-406B-83FB-897024CC711B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7034852$0CEFFC7D-2C20-4CFB-BE9C-E33810B9FDF9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"75952aae7585ff19bcc6e0780bb1ca054c1d56f5","datavalue":{"value":"7977165","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7034852$C904610E-FEC5-4BFE-BD4D-BD1F7FBE5897","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$50277595-6FA9-4ECB-BAF4-CBB2EDF08C88","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dac36a0d5bcef050bd5c5ec480998b0eb01458a6","datavalue":{"value":"SMT solving","type":"string"},"datatype":"string"},"type":"statement","id":"Q7034852$5AC7FE84-FCA7-45D1-A322-706C699778C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a943f58c8a70c390a9dd15496a4139fa7b432a9a","datavalue":{"value":"MCSat","type":"string"},"datatype":"string"},"type":"statement","id":"Q7034852$7F666FF6-C659-4F47-BF6B-795FDD7FA9E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac07c7d6c5cdc2dbc4590f3ecbac0ebb59196bea","datavalue":{"value":"finite fields","type":"string"},"datatype":"string"},"type":"statement","id":"Q7034852$4C8B7199-1740-4575-A3B4-010478B12157","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"10cb834e7a73184fb63f851df856fce5e4798475","datavalue":{"value":"polynomial arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q7034852$F9CF99E9-B5F8-4FAE-9839-0D4A7B02BFB4","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$78E6450F-7D3F-4C44-A71E-85B0F63638C0","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"67737023899dd2252d79885f477a3601bda6d265","datavalue":{"value":{"entity-type":"item","numeric-id":6114261,"id":"Q6114261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$923627C2-579C-4A30-A127-3A99FC733189","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48933c0d362727730cc1905c68ff87e3a22216cf","datavalue":{"value":{"entity-type":"item","numeric-id":2457345,"id":"Q2457345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$511F379A-C57A-43CE-B4A2-00207D9B7902","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"485257e2a8c4bb44d210af89ed8517de5ca7dfbf","datavalue":{"value":{"entity-type":"item","numeric-id":2248020,"id":"Q2248020"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$0F8B7D2B-8BF9-4CCA-A7E8-84B3ADCCE371","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae477ba2300400eec2908d55329cb4248dc074d4","datavalue":{"value":{"entity-type":"item","numeric-id":3833627,"id":"Q3833627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$A2073B33-6543-40FE-A02F-E60C3ADB40AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ef8a8532db5854f5d22fa31dcae929508b22146","datavalue":{"value":{"entity-type":"item","numeric-id":2096440,"id":"Q2096440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$70C1B18A-AE4A-4AE7-8AF3-9BE2292CD425","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cd7b0cc2fe1e93d1b3664031733149aae245bda","datavalue":{"value":{"entity-type":"item","numeric-id":7025216,"id":"Q7025216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$9BDF0A50-7CD2-488D-8720-219FF3DA9311","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fa4c2387ad30aeefcdaa752dcaca22072d33adf","datavalue":{"value":{"entity-type":"item","numeric-id":2961575,"id":"Q2961575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$083A9EE5-D9B5-437B-8594-858D5A863A03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d77121ca06023666fb3b31fe1611bc7b34ff56df","datavalue":{"value":{"entity-type":"item","numeric-id":2908506,"id":"Q2908506"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$2022057A-A64A-4AA2-96EE-F79301587694","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ddeddf292e13fd796c5c20e153357856b636f89","datavalue":{"value":{"entity-type":"item","numeric-id":2926635,"id":"Q2926635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$B3A03568-AA76-4CD4-BCCB-3B660771BC79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"103d28c1dbdf16ee025b2b302833c03273293813","datavalue":{"value":{"entity-type":"item","numeric-id":5705940,"id":"Q5705940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$6AF59EBB-67F5-4125-9725-23B264578422","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2a75c6518e96127fc24bfa25d866d94233173e90","datavalue":{"value":{"entity-type":"item","numeric-id":6535532,"id":"Q6535532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$C9DB6171-056D-482B-8386-CAE3DFE60483","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"80c8af58ee03b8048c50b2d28fa76b0f2a75becf","datavalue":{"value":{"entity-type":"item","numeric-id":6535685,"id":"Q6535685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$08B512EF-6892-441F-8097-501B52E8F0E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e4d80d10655647513f1efec0d8560effd4b94c30","datavalue":{"value":{"entity-type":"item","numeric-id":1125620,"id":"Q1125620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7034852$ED1BF58B-564B-42BA-98C7-67C5EF8439A8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:7034852","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:7034852"}}}}}