SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Solver Disagreements on UFNIA (Single Query Track)

Page generated on 2020-07-02 15:49:34 +0000

UFNIA/2019-Preiner/qf/f2_rw170.smt2

UFNIA/2019-Preiner/qf/f2_rw200.smt2

UFNIA/2019-Preiner/qf/f2_rw205.smt2

UFNIA/2019-Preiner/qf/f2_rw235.smt2

UFNIA/2019-Preiner/qf/f2_rw236.smt2

UFNIA/2019-Preiner/qf/f2_rw237.smt2

UFNIA/2019-Preiner/qf/f2_rw247.smt2

UFNIA/2019-Preiner/qf/f2_rw27.smt2

UFNIA/2019-Preiner/qf/f2_rw287.smt2

UFNIA/2019-Preiner/qf/f2_rw29.smt2

UFNIA/2019-Preiner/qf/f2_rw35.smt2

UFNIA/2019-Preiner/qf/f2_rw361.smt2

UFNIA/2019-Preiner/qf/f2_rw365.smt2

UFNIA/2019-Preiner/qf/f2_rw48.smt2

UFNIA/2019-Preiner/qf/f2_rw76.smt2

UFNIA/2019-Preiner/qf/f2_rw95.smt2

UFNIA/2019-Preiner/qf/t3_rw1001.smt2

UFNIA/2019-Preiner/qf/t3_rw1011.smt2

UFNIA/2019-Preiner/qf/t3_rw1088.smt2

UFNIA/2019-Preiner/qf/t3_rw1140.smt2

UFNIA/2019-Preiner/qf/t3_rw1199.smt2

UFNIA/2019-Preiner/qf/t3_rw1203.smt2

UFNIA/2019-Preiner/qf/t3_rw1234.smt2

UFNIA/2019-Preiner/qf/t3_rw1357.smt2

UFNIA/2019-Preiner/qf/t3_rw1420.smt2

UFNIA/2019-Preiner/qf/t3_rw1431.smt2

UFNIA/2019-Preiner/qf/t3_rw1522.smt2

UFNIA/2019-Preiner/qf/t3_rw1550.smt2

UFNIA/2019-Preiner/qf/t3_rw1553.smt2

UFNIA/2019-Preiner/qf/t3_rw22.smt2

UFNIA/2019-Preiner/qf/t3_rw224.smt2

UFNIA/2019-Preiner/qf/t3_rw244.smt2

UFNIA/2019-Preiner/qf/t3_rw258.smt2

UFNIA/2019-Preiner/qf/t3_rw266.smt2

UFNIA/2019-Preiner/qf/t3_rw34.smt2

UFNIA/2019-Preiner/qf/t3_rw342.smt2

UFNIA/2019-Preiner/qf/t3_rw432.smt2

UFNIA/2019-Preiner/qf/t3_rw460.smt2

UFNIA/2019-Preiner/qf/t3_rw537.smt2

UFNIA/2019-Preiner/qf/t3_rw616.smt2

UFNIA/2019-Preiner/qf/t3_rw626.smt2

UFNIA/2019-Preiner/qf/t3_rw71.smt2

UFNIA/2019-Preiner/qf/t3_rw817.smt2

UFNIA/2019-Preiner/qf/t3_rw862.smt2

UFNIA/2019-Zohar-ic/qf/int_check_bvult_bvlshr1_ltr_no_inv.smt2

UFNIA/2019-Zohar-ic/qf/int_check_bvult_bvudiv1_ltr_no_inv.smt2

n Non-competing.
u Solver is unsound in this division.