(declare-fun x ( ) String) 
(declare-fun i1 ( ) Int) 
(declare-fun i2 ( ) Int) 
(declare-fun i3 ( ) Int) 
(declare-fun i4 ( ) Int) 
(assert ( and ( < i1 8 ) ( < i2 100 ) ( > ( / 256 i1 i2 ) ( str.len x )))) 
(assert ( xor  ( <= i4 112 ) ( > ( * 227 i3 i4 ) ( str.len x )))) 
(assert ( = "efg" ( str.substr x i1 i2 ))) 
(assert ( distinct "bef" ( str.substr x i3 i4 ))) 
(assert ( > ( str.len x ) 91 )) (check-sat)    

$ CVC4/build/bin/cvc4 --quiet small.smt2 
sat
$ z3debug/build/z3 small.smt2 
unsat
$ cat small.smt2 
(declare-fun x ( ) String) 
(declare-fun i1 ( ) Int) 
(declare-fun i2 ( ) Int) 
(declare-fun i3 ( ) Int) 
(declare-fun i4 ( ) Int) 
(assert ( and ( < i1 8 ) ( < i2 100 ) ( > ( / 256 i1 i2 ) ( str.len x )))) 
(assert ( xor  ( <= i4 112 ) ( > ( * 227 i3 i4 ) ( str.len x )))) 
(assert ( = "efg" ( str.substr x i1 i2 ))) 
(assert ( distinct "bef" ( str.substr x i3 i4 ))) 
(assert ( > ( str.len x ) 91 )) (check-sat)