Install

1. Intall z3 prover
   1. Ubuntu

    xxx@XXX:~$ sudo apt install z3
   

   2. Other see Z3Prover
2. Install Rust: Rust
3. Install SMT-Language:

    xxx@XXX:~$ cargo install smt-lang
   

Run SMT-language

xxx@XXX:~$ smt-lang --file problem_file.sl

Options

Verbose

• --verbose 0 : display nothing
• --verbose 1 : display analysis result
• --verbose 2 : display loaded problem
• --verbose 3 : display SMT problem and SMT model if a solution is found

Syntax

Type

• Bool: boolean type
• Int: integer type (unbounded)
• Real: real type

Variable

let <identifier> : <Type> [= <Expression>]

Constraint

constraint <identifier> = <Expression>

Expression

soon

Example

Soon