text: #include <assert.h>
  #include <stdio.h>
  #include <stdlib.h>
  #include "boolector.h"
  
  #define BV1_EXAMPLE_NUM_BITS 8
  
  /* We verify the XOR swap algorithm. The XOR bitwise operation can
   * be used to swap variables without using a temporary variable:
   * int x, y;
   * ...
   * x = x ^ y
   * y = x ^ y
   * x = x ^ y
   */
  
  int
  main (void)
  {
    Btor *btor;
    BoolectorNode *x, *y, *temp, *old_x, *old_y, *eq1, *eq2, *and, *formula;
    BoolectorSort s;
    int result;
  
    btor = boolector_new ();
    s    = boolector_bitvec_sort (btor, BV1_EXAMPLE_NUM_BITS);
    x    = boolector_var (btor, s, NULL);
    y    = boolector_var (btor, s, NULL);
  
    /* remember initial values of x and y */
    old_x = boolector_copy (btor, x);
    old_y = boolector_copy (btor, y);
  
    /* x = x ^ y */
    temp = boolector_xor (btor, x, y);
    boolector_release (btor, x);
    x = temp;
  
    /* y = x ^ y */
    temp = boolector_xor (btor, x, y);
    boolector_release (btor, y);
    y = temp;
  
    /* x = x ^ y */
    temp = boolector_xor (btor, x, y);
    boolector_release (btor, x);
    x = temp;
  
    /* Now, we have to show that old_x = y and old_y = x */
    eq1 = boolector_eq (btor, old_x, y);
    eq2 = boolector_eq (btor, old_y, x);
    and = boolector_and (btor, eq1, eq2);
  
    /* In order to prove that this is a theorem, we negate the whole
     * formula and show that the negation is unsatisfiable */
    formula = boolector_not (btor, and);
  
    /* We assert the formula and call Boolector */
    boolector_assert (btor, formula);
    result = boolector_sat (btor);
    printf ("Expect: unsat\n");
    printf ("Boolector: %s\n",
            result == BOOLECTOR_SAT
                ? "sat"
                : (result == BOOLECTOR_UNSAT ? "unsat" : "unknown"));
    if (result != BOOLECTOR_UNSAT) abort ();
  
    /* cleanup */
    boolector_release (btor, x);
    boolector_release (btor, old_x);
    boolector_release (btor, y);
    boolector_release (btor, old_y);
    boolector_release (btor, eq1);
    boolector_release (btor, eq2);
    boolector_release (btor, and);
    boolector_release (btor, formula);
    boolector_release_sort (btor, s);
    assert (boolector_get_refs (btor) == 0);
    boolector_delete (btor);
    return 0;
  }
  