regehr

from z3 import *

# find the (distinct) integers in 0..9 that make this equation work:                                              
#                                                                                                                 
#   SEND                                                                                                          
# + MORE                                                                                                          
# ------                                                                                                          
#  MONEY                                                                                                          

S = Int('S')

regehr

#include <assert.h>

int main(void) {
  unsigned i = 0;
  do {
    assert((i / 4532) == (i * 0x39D7C7F7ULL) >> 42);
    i++;
  } while (i);
}

regehr

(set-logic QF_BV)
(set-info :status unknown)
(declare-fun x () (_ BitVec 32))
(assert
 (and (distinct (bvudiv x (_ bv4532 32)) ((_ extract 31 0) (bvlshr (bvmul ((_ zero_extend 32) x) ((_ zero_extend 32) (_ bv970442743 32))) (_ bv42 64)))) true))
(check-sat)

regehr

from z3 import *

def make_lhs(x):
    lhs = UDiv(x, BitVecVal(4532, 32))
    return lhs

def make_rhs(x, c):
    t1 = ZeroExt(32, x)
    tc = ZeroExt(32, c)
    t2 = t1 * tc

regehr

Johns-MacBook-Pro-3:code regehr$ clang++ -O3 hello.cpp 
../tools/clang/lib/Sema/SemaExpr.cpp:15061:43: runtime error: implicit conversion from type 'unsigned long' of value 18446744073709551615 (64-bit, unsigned) to type 'const unsigned int' changed the value to 4294967295 (32-bit, unsigned)
../lib/IR/LLVMContextImpl.h:184:12: runtime error: implicit conversion from type 'size_t' (aka 'unsigned long') of value 6885126708080135535 (64-bit, unsigned) to type 'unsigned int' changed the value to 346803567 (32-bit, unsigned)
../include/llvm/Support/MathExtras.h:540:10: runtime error: implicit conversion from type 'unsigned long' of value 18446744073709551615 (64-bit, unsigned) to type 'unsigned int' changed the value to 4294967295 (32-bit, unsigned)
../lib/IR/LLVMContextImpl.cpp:197:10: runtime error: implicit conversion from type 'size_t' (aka 'unsigned long') of value 2306719784053904382 (64-bit, unsigned) to type 'unsigned int' changed the value to 216404990 (32-bit, unsigned)
../lib/IR/ConstantsContext.h:522:1

regehr

from z3 import *

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
             for i in range(9) for j in range(9) ]

regehr

from z3 import *

# find autobiographical numbers                                                                                                

def auto(lim):
  if lim < 1 or lim > 10:
    raise Exception('only 1..10 are valid arguments')

  print str(lim) + ":"

regehr

from z3 import *

# find autobiographical numbers                                                                                                

def auto(lim):
  if lim < 1 or lim > 10:
    raise Exception('only 1..10 are valid arguments')

  print str(lim) + " : ",

regehr

TeX log appears below

[verbose]: Creating arXiv submission AutoTeX object
[verbose]: *** Using TeX Live 2016 ***
[verbose]: Calling arXiv submission AutoTeX process
[verbose]: TeX/AutoTeX.pm: admin_timeout = minion
[verbose]: <fig1-cropped.pdf>	is of type 'PDF'.
[verbose]: <paper.bbl>	is of type 'TeX auxiliary'.
[verbose]: <intro.tex>	is of type 'TEX'.
[verbose]: <souper.tex>	is of type 'TEX'.

regehr

FAIL: Souper :: Pass/syn-inst-zext.ll (196 of 345)
******************** TEST 'Souper :: Pass/syn-inst-zext.ll' FAILED ********************
Script:
--
/home/regehr/souper-rsas/third_party/llvm/Debug/bin/llvm-as -o /home/regehr/souper-rsas/build/test/Pass/Output/syn-inst-zext.ll.tmp /home/regehr/souper-rsas/test/Pass/syn-inst-zext.ll
/home/regehr/souper-rsas/third_party/llvm/Debug/bin/opt -load /home/regehr/souper-rsas/build/libsouperPass.so -souper -dce -z3-path=/usr/bin/z3 -souper-infer-inst -S -o - /home/regehr/souper-rsas/test/Pass/syn-inst-zext.ll | /home/regehr/souper-rsas/third_party/llvm/Debug/bin/FileCheck /home/regehr/souper-rsas/test/Pass/syn-inst-zext.ll
--
Exit Code: 2

Command Output (stderr):