SMT-LIB

Contact owners and managers

1–30 of 97

This is a technical discussion forum for the SMT-LIB initiative. The major goal of SMT-LIB is to promote common standards and maintain a library of benchmarks for SMT solvers.

More information on SMT-LIB can be found on the SMT-LIB website.

If you want to join the group please provide both your first and your last name.

Note: Before May 30, 2017, this forum was hosted on a different server. See the SMT-LIB Archives for posts made on that server.

Important: Please do not post announcements (conference, positions, etc.) on this forum. Use SMT-announce instead.

0 selected

Apr 13

SMT 2024 Third Call For Papers

======================================================== SMT 2024: 22nd International Workshop on

unread,

SMT 2024 Third Call For Papers

======================================================== SMT 2024: 22nd International Workshop on

Apr 13

Mikoláš Janota, Clark Barrett2

Mar 27

Semantics for "(set-info :status sat/unsat")

We have not made this distinction. We allow both, but periodically do try to confirm as many as

unread,

Semantics for "(set-info :status sat/unsat")

We have not made this distinction. We allow both, but periodically do try to confirm as many as

Mar 27

Mar 15

SMT 2024 Call For Papers

======================================================== SMT 2024: 22nd International Workshop on

unread,

SMT 2024 Call For Papers

======================================================== SMT 2024: 22nd International Workshop on

Mar 15

Mathias Preiner, … BOBOT Francois7

Mar 8

SMT-LIB Benchmarks on Zenodo

Le jeudi 15 février 2024 à 10:31 -0800, Clark Barrett a écrit : One DOI per year sounds like a good

unread,

SMT-LIB Benchmarks on Zenodo

Le jeudi 15 février 2024 à 10:31 -0800, Clark Barrett a écrit : One DOI per year sounds like a good

Mar 8

Martin Bromberger

Feb 19

SMT-COMP 2024: Preliminary Call for Solvers

Hello everybody, The submission deadline for the first version of the solvers is on May 27. However,

unread,

SMT-COMP 2024: Preliminary Call for Solvers

Hello everybody, The submission deadline for the first version of the solvers is on May 27. However,

Feb 19

Martin Bromberger

Feb 19

Call for Benchmarks 2024

Hello! Do you have interesting or hard benchmarks that can be made public? Want the world's best

unread,

Call for Benchmarks 2024

Hello! Do you have interesting or hard benchmarks that can be made public? Want the world's best

Feb 19

Pascal Fontaine, … Clark Barrett10

11/29/23

FixedSizeBitVectors, QF_BV, overflows

Dear All, thanks for the comments. There has been some progress on this issue, and there is a

unread,

FixedSizeBitVectors, QF_BV, overflows

Dear All, thanks for the comments. There has been some progress on this issue, and there is a

11/29/23

Dennis Yurichev, Aaron Stump2

11/15/23

Hi, Dennis. I notice that on StarExec, there is a SyGuS-Comp19 folder, but it is not public. Best,

unread,

Hi, Dennis. I notice that on StarExec, there is a SyGuS-Comp19 folder, but it is not public. Best,

11/15/23

Dennis Yurichev, Clark Barrett2

11/9/23

Getting all SMT benchmarks

The UIowa gitlab repositories have the latest benchmarks and cloning them is the recommended way to

unread,

Getting all SMT benchmarks

The UIowa gitlab repositories have the latest benchmarks and cloning them is the recommended way to

11/9/23

Christoph Wintersteiger, … Mak Andrlon4

11/6/23

Rounding of to_fp from signed bit-vectors

Thanks for the pointer, Mak! I had forgotten that this exception is right there in '754.

unread,

Rounding of to_fp from signed bit-vectors

Thanks for the pointer, Mak! I had forgotten that this exception is right there in '754.

11/6/23

erk...@gmail.com, Clark Barrett4

6/23/23

Can theory symbols be overloaded by user scripts?

I can see why the second sentence might cause some confusion. I'll propose a fix to the team. -

unread,

Can theory symbols be overloaded by user scripts?

I can see why the second sentence might cause some confusion. I'll propose a fix to the team. -

6/23/23

Jochen Hoenicke

5/18/23

[SMT-COMP] StarExec Test Jobs Started

Hi SMT community, We have received 25 solver submissions. Please check the website if the data for

unread,

[SMT-COMP] StarExec Test Jobs Started

Hi SMT community, We have received 25 solver submissions. Please check the website if the data for

5/18/23

2/15/23

New divisions in the Model-Validation Track

Hello! we want to try out some new, experimental divisions in the Model-Validation Track of future

unread,

New divisions in the Model-Validation Track

Hello! we want to try out some new, experimental divisions in the Model-Validation Track of future

2/15/23

2/7/23

Fwd: [smt-announce] SMT-COMP 2023: Call for solvers

---------- Forwarded message --------- From: BOBOT Francois <Francoi...@cea.fr> Date: Tue,

unread,

Fwd: [smt-announce] SMT-COMP 2023: Call for solvers

---------- Forwarded message --------- From: BOBOT Francois <Francoi...@cea.fr> Date: Tue,

2/7/23

2/7/23

Call for benchmarks 2023

Hello! Do you have interesting or hard benchmarks that can be made public? Want the world's best

unread,

Call for benchmarks 2023

Hello! Do you have interesting or hard benchmarks that can be made public? Want the world's best

2/7/23

8/10/22

[SMT-COMP] Results online

Hello, The results of SMT-COMP are online: https://smt-comp.github.io/2022 At FLoC we had special

unread,

[SMT-COMP] Results online

Hello, The results of SMT-COMP are online: https://smt-comp.github.io/2022 At FLoC we had special

8/10/22

7/6/22

[SMT-COMP] The competition has started

Hello, The SMT-COMP 2022 is live. You can follow it on StarExec: https://www.starexec.org/starexec/

unread,

[SMT-COMP] The competition has started

Hello, The SMT-COMP 2022 is live. You can follow it on StarExec: https://www.starexec.org/starexec/

7/6/22

Jochen Hoenicke

7/3/22

SMT-COMP solver deadline is approaching

Dear SMT community, This is a reminder that the SMT-COMP final solver deadline is in a few hours (

unread,

SMT-COMP solver deadline is approaching

Dear SMT community, This is a reminder that the SMT-COMP final solver deadline is in a few hours (

7/3/22

Jochen Hoenicke

6/28/22

SMT-COMP 2022 More Test Jobs

Dear SMT community, I have started a second run of test jobs for the four traditional tracks on

unread,

SMT-COMP 2022 More Test Jobs

Dear SMT community, I have started a second run of test jobs for the four traditional tracks on

6/28/22

6/27/22

Zulip channel for SMT discussions

Hello, In a discussion on the SMT proofs group it was suggested that we had a zulip organization to

unread,

Zulip channel for SMT discussions

Hello, In a discussion on the SMT proofs group it was suggested that we had a zulip organization to

6/27/22

Jochen Hoenicke

6/21/22

SMT-COMP Test Runs

Hello, as Haniel already mentioned the first test runs are available here: https://www.starexec.org/

unread,

SMT-COMP Test Runs

Hello, as Haniel already mentioned the first test runs are available here: https://www.starexec.org/

6/21/22

6/20/22

[SMT-COMP] List of participants online and test jobs

Hello, The list of submitted solvers to SMT-COMP is now online https://smt-comp.github.io/2022/

unread,

[SMT-COMP] List of participants online and test jobs

Hello, The list of submitted solvers to SMT-COMP is now online https://smt-comp.github.io/2022/

6/20/22

6/1/22

[SMT-COMP] Final call for solvers

=============================================================== 17th International Satisfiability

unread,

[SMT-COMP] Final call for solvers

=============================================================== 17th International Satisfiability

6/1/22

Mathias Preiner2

5/25/22

SMT-LIB benchmark release 2022

Hi all, The new release is now available on StarExec: https://www.starexec.org/starexec/secure/

unread,

SMT-LIB benchmark release 2022

Hi all, The new release is now available on StarExec: https://www.starexec.org/starexec/secure/

5/25/22

3/22/22

[SMT-COMP] Call for solvers

Hello everybody, The submission deadline for the first version of the solvers is on Jun 18. However,

unread,

[SMT-COMP] Call for solvers

Hello everybody, The submission deadline for the first version of the solvers is on Jun 18. However,

3/22/22

2/22/22

[SMT-COMP] Call for comments

Dear SMT-COMP participants, dear SMT-LIB community, We are happy to announce the plans for the

unread,

[SMT-COMP] Call for comments

Dear SMT-COMP participants, dear SMT-LIB community, We are happy to announce the plans for the

2/22/22

2/9/22

[SMT-COMP] Call for benchmarks

Hello! Do you have interesting or hard benchmarks that can be made public? Want the world's best

unread,

[SMT-COMP] Call for benchmarks

Hello! Do you have interesting or hard benchmarks that can be made public? Want the world's best

2/9/22

Clark Barrett, … Cesare Tinelli19

1/31/22

New working group on SMT proofs

Dear member of the SMT community, Thanks to all who have expressed their interest in joining a

unread,

New working group on SMT proofs

Dear member of the SMT community, Thanks to all who have expressed their interest in joining a

1/31/22

of...@ie.technion.ac.il, … Vijay Ganesh5

11/4/21

Looking for Modeling questions in SMT, for students

Yes, Dennis' books is excellent. I am using it as part of my SAT/SMT course. Warm Regards, Vijay

unread,

Looking for Modeling questions in SMT, for students

Yes, Dennis' books is excellent. I am using it as part of my SAT/SMT course. Warm Regards, Vijay

11/4/21

Siyuan Chen, … Viktor Kunčak3

11/1/21

Define mutually recursive functions in SMTLIB 3.0?

The expanding definition of SMT-LIB 3.0 continues to be exciting to me. :) It says somewhere that it

unread,

Define mutually recursive functions in SMTLIB 3.0?

The expanding definition of SMT-LIB 3.0 continues to be exciting to me. :) It says somewhere that it

11/1/21

Search

Clear search

Close search

Google apps

Main menu