From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.9 required=5.0 tests=DNS_FROM_RFC_ABUSE, HTML_MESSAGE,SPF_SOFTFAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 3952DBC69 for ; Wed, 24 Oct 2007 21:00:17 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAANIyH0eDa3PXn2dsb2JhbACCcotoAgEBBwQGCQgY X-IronPort-AV: E=Sophos;i="4.21,326,1188770400"; d="scan'208,217";a="18571340" Received: from smtp.microsoft.com ([131.107.115.215]) by mail4-smtp-sop.national.inria.fr with ESMTP; 24 Oct 2007 21:00:15 +0200 Received: from tk5-exhub-c104.redmond.corp.microsoft.com (157.54.70.185) by TK5-EXGWY-E802.partners.extranet.microsoft.com (10.251.56.168) with Microsoft SMTP Server (TLS) id 8.1.222.3; Wed, 24 Oct 2007 12:00:13 -0700 Received: from tk5-exmlt-w602.wingroup.windeploy.ntdev.microsoft.com (157.54.70.14) by tk5-exhub-c104.redmond.corp.microsoft.com (157.54.70.185) with Microsoft SMTP Server id 8.1.177.1; Wed, 24 Oct 2007 12:00:05 -0700 Received: from TK5-EXMLT-W603.wingroup.windeploy.ntdev.microsoft.com (157.54.18.6) by TK5-EXMLT-W602.wingroup.windeploy.ntdev.microsoft.com (157.54.70.14) with Microsoft SMTP Server (TLS) id 8.1.122.1; Wed, 24 Oct 2007 11:59:58 -0700 Received: from NA-EXMSG-W601.wingroup.windeploy.ntdev.microsoft.com ([fe80::5efe:10.255.255.1]) by TK5-EXMLT-W603.wingroup.windeploy.ntdev.microsoft.com ([157.54.18.6]) with mapi; Wed, 24 Oct 2007 11:59:58 -0700 From: Nikolaj Bjorner To: "caml-list@yquem.inria.fr" Cc: Leonardo de Moura Date: Wed, 24 Oct 2007 11:59:56 -0700 Subject: Z3 version 1.1. Thread-Topic: Z3 version 1.1. Thread-Index: AcgWcBFf/vL23tNJR7K5gjBbkFja5g== Message-ID: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: acceptlanguage: en-US Content-Type: multipart/alternative; boundary="_000_DBCE3290C3BA8647A9D90EEEFA1C48ADEEA8912C3ANAEXMSGW601wi_" MIME-Version: 1.0 X-Spam: no; 0.00; bjorner:01 smt:01 extensional:01 arrays:01 quantifiers:01 low-level:01 ocaml:01 bjorner:01 smt:01 extensional:01 arrays:01 quantifiers:01 low-level:01 ocaml:01 integer:01 --_000_DBCE3290C3BA8647A9D90EEEFA1C48ADEEA8912C3ANAEXMSGW601wi_ Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable We are pleased to announce of Z3 version 1.1. Z3 is a new high-performance theorem prover for Satisfiability Modulo Theories (SMT) problems being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 has already been integrated in several projects and products at Microsoft. It can read problems in SMT-LIB, Simplify and a native low-level format. Z3 can also be invoked programmatically from either C/C++, OCaml or from .NET. More information about Z3, including download links are available from: http://research.microsoft.com/projects/z3 Kind regards, Leonardo de Moura and Nikolaj Bjorner. --_000_DBCE3290C3BA8647A9D90EEEFA1C48ADEEA8912C3ANAEXMSGW601wi_ Content-Type: text/html; charset="us-ascii" Content-Transfer-Encoding: quoted-printable

We are pleased to announce of Z3 version 1.1.

Z3 is a new high-performance theorem prover for Satisfiability Modulo

Theories (SMT) problems being developed at Microsoft Research. = Z3

supports linear real and integer arithmetic, fixed-size bit-vectors,

extensional arrays, uninterpreted functions, and quantifiers. Z= 3 has

already been integrated in several projects and products at

Microsoft. It can read problems in SMT-LIB, Simplify and a nati= ve

low-level format. Z3 can also be invoked programmatically from either

C/C++, OCaml or from .NET.

More information about Z3, including download links are availab= le from:

http://re= search.microsoft.com/projects/z3

Kind regards,

Leonardo de Moura and Nikolaj Bjorner.

--_000_DBCE3290C3BA8647A9D90EEEFA1C48ADEEA8912C3ANAEXMSGW601wi_--