gavlegoat

(declare-fun t1 () Int)
(declare-fun t2 () Int)
(declare-fun t3 () Int)
(declare-fun t4 () Int)
(declare-fun t5 () Int)
(declare-fun t6 () Int)

(assert
(and
(> (+ (- (+ t3 (* 1.000000 t4)) (* 4 t5)) (* 16.000000 t6)) 0)

gavlegoat

#include "dreal/dreal.h"

int main() {
  dreal::Variable tmp_var0("t1", dreal::Variable::Type::INTEGER);
  dreal::Variable tmp_var1("t2", dreal::Variable::Type::INTEGER);
  dreal::Variable tmp_var2("t3", dreal::Variable::Type::INTEGER);
  dreal::Variable tmp_var3("t4", dreal::Variable::Type::INTEGER);
  dreal::Variable tmp_var4("t5", dreal::Variable::Type::INTEGER);
  dreal::Variable tmp_var5("t5", dreal::Variable::Type::INTEGER);

gavlegoat

#include <t1p.h>
#include <ap_abstract0.h>

#include <stdio.h>

/* This is an example to demonstrate a bug in Apron's taylor1plus domain. We
 * maintain two abstract values, v1 and v2. In a loop we do the following:
 * - Append v2 to v1 to generate a new abstract value with dimension equal to
 *   the sum of the dimensions of v1 and v2.
 * - Perform a linear assignment on this abstract value.

gavlegoat

#include <t1p.h>
#include <ap_abstract0.h>

int main(int argc, char** argv) {

  ap_manager_t* man = t1p_manager_alloc();

  int in_size = 10;
  int out_size = 5;
  ap_interval_t** itv = ap_interval_array_alloc(in_size);

gavlegoat

#include <iostream>
#include <opt_oct.h>

int main() {
  elina_manager_t* man = opt_oct_manager_alloc();

  elina_interval_t** itv1 = (elina_interval_t**) malloc(2 *
      sizeof(elina_interval_t*));

  itv1[0] = elina_interval_alloc();