smcc

#include <errno.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <time.h>
#include <sys/time.h>
#include <unistd.h>

int main(int argc, char **argv) {
    struct timespec ts;

smcc

#include "c_interface.h"

void test(void) {
    VC vc = vc_createValidityChecker();
    vc_setInterfaceFlags(vc, (ifaceflag_t)0, 0);
    vc_push(vc);
    Type ty_bv8 = vc_bvType(vc, 8);
    Type ty_bv16 = vc_bvType(vc, 16);
    Type ty_bv32 = vc_bvType(vc, 32);

smcc

(set-logic QF_BV)
(declare-fun _substvar_63535_ () Bool)
(declare-fun _substvar_11241_ () (_ BitVec 8))
(declare-fun _substvar_11228_ () (_ BitVec 8))
(declare-fun _substvar_11223_ () (_ BitVec 8))
(declare-fun _substvar_58110_ () (_ BitVec 32))
(declare-fun _substvar_11243_ () (_ BitVec 8))
(declare-fun _substvar_11242_ () (_ BitVec 8))
(declare-fun _substvar_74320_ () Bool)
(declare-fun _substvar_61240_ () (_ BitVec 32))

smcc

% Trimmed-down example that triggers failures in many different
% STP versions because it causes STP to think about dividing
% by zero.

y : BV(8);

% Should be equivalent to "t4 : BV(8) = 0h01":
t4 : BV(8) = BVPLUS(8, y, BVUMINUS(y), 0h01);

% Should be invalid. Definitely by y = 0h01, but potentially