ajreynol
commented
3 years ago The commit bd2793a fixed a refutation soundness bug. That commit was a straightforward fix of a lemma that was unsound. Thus if CVC4 solved this quickly before that commit and does not solve now, it may have been due to unsound reasoning.
Thus, I'd classify this as "performance".
(set-logic QF_SLIA) (declare-fun var0 () String) (declare-fun var1 () String) (declare-fun var2 () String) (declare-fun var3 () String) (declare-fun var4 () String) (declare-fun var5 () String) (declare-fun var6 () String) (declare-fun var7 () String) (declare-fun var8 () String) (declare-fun var11 () String) (declare-fun var12 () String) (declare-fun var13 () String) (declare-fun var14 () String) (declare-fun var15 () String) (declare-fun var16 () String) (declare-fun var17 () String) (declare-fun var18 () String) (declare-fun var19 () String) (declare-fun var22 () String) (declare-fun var23 () String) (declare-fun var24 () String) (declare-fun var25 () String) (declare-fun var26 () String) (declare-fun var29 () String) (declare-fun var9 () Int) (declare-fun var10 () Int) (declare-fun var20 () Int) (declare-fun var21 () Int) (declare-fun var27 () Int) (declare-fun var28 () Int) (assert (not (str.prefixof (str.++ (str.++ var0 var1) (str.++ var2 var3)) (str.at (str.++ var2 var2) (str.len var4))))) (assert (str.contains (str.++ var4 var5) (str.replace var5 var7 var6))) (assert (and (not (< (str.len var8) (str.len var1))) (or (not (<= var9 4)) (< var10 9)))) (assert (< (str.len (str.replace var11 var13 var12)) (str.len (str.replace var14 var16 var15)))) (assert (str.prefixof (str.substr var5 0 1) (str.++ var1 var5))) (assert (not (>= (str.indexof var5 var17 var10) (str.len var2)))) (assert (str.contains (str.substr (str.++ var5 var2) (- (str.indexof var15 var6 var10) (- 10)) (+ (str.len var5) 12)) (str.substr (str.++ (str.replace var2 var18 var5) (str.replace var2 var19 var14)) 1 38))) (assert (= (or (> var20 4) (> var21 5)) (not (= (str.len var11) (str.indexof var22 var23 var21))))) (assert (= (str.indexof var24 var25 var21) (str.indexof var12 var26 var21))) (assert (and (or (>= var27 0) (> var28 3)) (str.contains (str.replace var2 var29 var2) (str.substr var5 0 1)))) (assert (= var17 "sa79TAXojiXEB88oHJn7")) (assert (= var20 7)) (assert (= var5 "77sa79TAXojiXEB88oHJnsa79TAXojiXEB88oHJn")) (check-sat)
CVC4-1.8 :10.5s CVC4-1.9 : more than 300s we also find the commit which caused this issue: bd2793a68e021ab58ab07db0cac67cf3d6806ead Could you please let me know if this regression is a compromise or totally a bug?