dblotsky / stringfuzz

Fuzzer and generator for string and regex problems in SMT-LIB 2.x format.
Other
20 stars 9 forks source link

Bandit Issue #2 #42

Open j29scott opened 5 years ago

j29scott commented 5 years ago

Command:

stringfuzzx --file /tmp/tmpuu5r6x7i --random bandit --operator 'IndexOf2' Input:

 (set-logic QF_S)
(declare-fun var0 () String)
(declare-fun var1 () String)
(declare-fun var2 () String)
(declare-fun var3 () Int)
(declare-fun var4 () Int)
(declare-fun var5 () Int)
(declare-fun var6 () Bool)
(declare-fun var7 () Bool)
(declare-fun var8 () Bool)
(assert (> var4 var4))
(assert (< (str.indexof var0 var2 var5) (str.len var2)))
(assert (>= (str.len var0) (str.indexof var2 var2 var4)))
(assert (< (str.len var2) (str.indexof var1 var1 var3)))
(assert (not var6))
(check-sat)