
-- Declaration of symbols
Sat

-- Adding some assertions (uses methods from IExpression._)
Sat

-- Querying the model
r = true
r & !s = false
v = true

-- Scoping (locally add assertions, declare symbols, etc)
Unsat
Sat

-- Shorter notation via importing
Sat
Sat

-- Nesting scopes and use of quantifiers
Unsat

-- Declaring functions
Sat
f(x) + f(z) = -1
(f(x) === f(z)) = false
Unsat

-- Generating different models for the same formula
  p1  	  p2  	  p3
------------------------
  -	  true	  true
  true	  true	  false

-- Incremental solving
  p1  	  p2  	  p3
------------------------
  true	  true	  true
  false	  true	  true
  true	  true	  false

-- Validity mode
Sat
x = 6
2*x = 12
Valid

-- Theory of arrays
Sat
select(a, 1) = 1
select(a, 10) = 0
Unsat
Valid
Unsat

-- Non-trivial quantifiers
Invalid
Valid

-- Quantifiers, functions, and triggers
Sat
b = -2
Unsat
Sat
b = -2
b = -3
b = -4
b = -5

-- Existential constants
Valid
X = 1
X + Y = 1
Y = 0
Valid
X = 10

-- Quantifier elimination
Valid
Equivalent qf constraint: X >= 4
Valid
Equivalent qf constraint: X = 42 | X = 3
Valid
Equivalent qf constraint: X = 42 | X = 3 | (X = 100 & Y >= 100)

-- Asynchronous interface
Running
Running
Sat

-- Asynchronous interface, timeouts
Running
Running
Sat

-- Asynchronous interface, busy waiting
Running
Sat

-- Stopping computations
expected result

-- Stopping computation after a while
expected result
Wait for 30ms ...
Sat

-- Interpolation
Unsat
Vector(c >= 0, d >= 1)
Vector(d - c >= 1, d >= 1)

-- Interpolation with functions
Unsat
Vector(!(c = 3) | f(3) >= 5, f(3) >= 5)
Vector(!(c = 3))

-- Interpolation with arrays
Unsat
Vector(!(select1(b, 0) = 2))

-- Generating a larger amount of constraints
Sat
c100 = 100
Valid

-- Generating a larger amount of constraints (2)
Sat
x500 = 124750
Valid

-- Declaration of symbols
Sat

-- Adding some assertions (uses methods from TerForConvenience._)
Sat
Unsat
Sat
Invalid
Valid
Sat
Sat
