Yices 1 Examples

These examples are not benchmarks. Their purpose is to illustrate Yices. If you are intererested in benchmarks, you should go to SMT-LIB.

Trivial

• trivial 1
• trivial 2
• trivial 3

Scalars

• scalar 1
• scalar 2
• scalar 3
• scalar 4
• scalar 5
• scalar 6
• scalar 7
• scalar 8
• scalar 9
• scalar 10
• scalar 11
• scalar 12
• scalar 13
• scalar 14
• scalar 15

Uninterpreted Types

• uninterpreted 1
• uninterpreted 2

Linear Arithmetic

• linear 1
• linear 2
• linear 3
• linear 4
• linear 5
• linear 6
• linear 7
• linear 8
• linear 9
• linear 10
• linear 11
• linear 12
• linear 13
• linear 14

Subtypes & Dependent Types

• type 1
• type 2
• type 3
• type 4
• type 5
• type 6
• type 7

Booleans as Terms

• bool 1
• bool 2
• bool 3

Function Updates (i.e., "Array Theory")

• array 1
• array 2
• array 3
• array 4
• array 5
• array 6
• array 7
• array 8
• array 9
• array 10
• array 11
• array 12
• array 13
• array 14
• array 15
• array 16
• array 17
• array 18
• array 19
• array 20
• array 21

Integer Completeness

• int 1
• int 2
• int 3
• int 4
• int 5
• int 6
• int 7
• int 8
• int 9
• int 10
• int 11
• int 12
• int 13
• int 14
• int 15
• int 16
• int 17
• int 18

Lambda Expressions

• lambda 1
• lambda 2
• lambda 3
• lambda 4
• lambda 5
• lambda 6
• lambda 7

Tuples

• tuple 1
• tuple 2
• tuple 3
• tuple 4
• tuple 5
• tuple 6
• tuple 7
• tuple 8

Records

• record 1
• record 2
• record 3
• record 4
• record 5
• record 6
• record 7
• record 8
• record 9
• record 10

Bit-vectors

• bv 1
• bv 2
• bv 3
• bv 4
• bv 5
• bv 6
• bv 7
• bv 8
• bv 9
• bv 10

Inductive datatypes

• datatype 1
• datatype 2
• datatype 3
• datatype 4
• datatype 5
• datatype 6
• datatype 7
• datatype 8
• datatype 9
• datatype 10
• datatype 11
• datatype 12
• datatype 13
• datatype 14
• datatype 15
• datatype 16
• datatype 17
• datatype 18

Quantifiers

• quant 1
• quant 2
• quant 3
• quant 4
• quant 5
• quant 6
• quant 7
• quant 8
• quant 9
• quant 10
• quant 11
• quant 12