Mr-Slippery

#ifdef KLEE
#include <klee/klee.h>
#include <assert.h>
#endif

#ifndef KLEE
#include <string.h>
#include <stdio.h>
#endif

Mr-Slippery

#include <klee/klee.h>
#include <assert.h>

#define N (15)

#define SYM(x) { \
  klee_make_symbolic(&x, sizeof x, #x); \
}

int main() {

Mr-Slippery

#include <klee/klee.h>
#include <assert.h>

typedef enum {
  NAT = 0,
  COL = 1,
  PET = 2,
  DRI = 3,
  SMO = 4
} cols_type;

Mr-Slippery

#include <klee/klee.h>
#include <assert.h>

#define N 8
unsigned char queens[N];

int abs(int x)
{
  return x >= 0 ? x: -x;
}

Mr-Slippery

#include <klee/klee.h>
#include <assert.h>

typedef unsigned char byte;

#define N 5

byte a[N * N]=
{
/*   A B C D E*/

Mr-Slippery

#!/usr/bin/env bash
set -euo pipefail

FILE=${1-main.cc}

if [ ! -f "${FILE}" ]
then
cat << EOF > "${FILE}"
#include <klee/klee.h>
#include <assert.h>

Mr-Slippery

extern crate num;

use num::complex::Complex;

struct IFS
{
    max_iter: u64
}

trait DDS<State> {

Mr-Slippery

#include <type_traits>

#define HAS_MEMBER(member) \
template <typename T, typename = void> \
struct has_##member : std::false_type {}; \
template <typename T> \
struct has_##member<T, std::void_t<decltype(std::declval<T>().member)>> : std::true_type {};

struct WithBla {
    int bla;

Mr-Slippery

#!/usr/bin/env python3
"""
Find counter examples to the conjecture:
The orbit of all strictly positive natural numbers
through col3 ends up in either C[0] and C[1].
"""
# Ignores PEP8 and pylint for brevity and math-friendly notation.

import sys

Mr-Slippery

#ifdef KLEE
#include <klee/klee.h>
#include <assert.h>
#endif

#include <stdbool.h>

#ifndef KLEE
#include <stdio.h>
#endif