Project

General

Profile

Skype Meeting 24-05-2016

Current Tasks:
  • LRA Interpolation
  • OpenSMT2 merge
  • Benchmarks on Git
  • SSA -> SMT - Finish the structure for Decl. part
  • Milestone I
  • Remove non-linearity from funfrog
Future Tasks:
  1. Search+uploading Benchmarks to Git
  2. Funfrog + Parallelizm
  3. EUF with Predicats (True/False P(x))
    Example of its use (as was on the Skype meeting)
    P( x )
    P( y )
    P( x ) := (x*x)
    x = y
    P( x ) = P( y )
    P( x ) := (x * x > 3)
    P( x ) == false
    P( z )
    P( z ) != P( y )
    P( z ) != P( x )