We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Hello everyone,
it seems that eldarica returns an invalid model for the following code:
(declare-fun pl24 ( ( Array Int ( Array Int Int ) ) Bool ) Bool) (declare-fun pbool ( Bool ) Bool) (assert ( pbool false )) (assert (forall ( ( m ( Array Int ( Array Int Int ) ) ) ) ( => ( pl24 m true ) false ))) (assert (forall ( ( m ( Array Int ( Array Int Int ) ) ) ( aq Bool ) ( ar1 ( Array Int ( Array Int Int ) ) ) ( ar2 ( Array Int Int ) ) ) ( => ( and ( pbool aq ) ( = m ( store ar1 1 ( store ar2 ( + ( ite ( <= ( mod ( + 5 ( mod 5 6 ) ) 6 ) 7 ) ( mod ( + ( mod 5 6 ) ) 6 ) 2 ) ) 0 ) ) ) ) ( pl24 m aq ) ))) (check-sat)
If I call ~/eldarica/eld -ssol test.smt2 I get
~/eldarica/eld -ssol test.smt2
sat ( (define-fun pbool ((A Bool)) Bool (not (= A true))) (define-fun pl24 ((A (Array Int (Array Int Int))) (B Bool)) Bool (and (or (exists ((var0 Int)) (exists ((var1 Int)) (and (and (exists ((var2 Int)) (and (and (<= (* 6 var2) 5) (>= (* 6 var2) 0)) (and (and (>= (+ (* (- 6) var2) (* (- 6) var1)) (- 10)) (>= (+ (* 6 var2) (* 6 var1)) 5)) (>= (+ (* 6 var2) (* 6 var1)) 3)))) (and (and (<= (* 6 var1) 5) (>= (* 6 var1) 0)) (and (>= (+ (* (- 6) var1) (* (- 6) var0)) (- 5)) (>= (* 6 var1) (* (- 6) var0))))) (= (select (select A 1) (+ 5 (+ (* (- 6) var1) (* (- 6) var0)))) 0)))) (exists ((var0 (Array Int Int))) (exists ((var1 Int)) (exists ((var2 Int)) (exists ((var3 Int)) (exists ((var4 (Array Int (Array Int Int)))) (exists ((var5 Int)) (and (and (and (and (<= (* 6 var3) 5) (>= (* 6 var3) 0)) (and (and (>= (+ (* (- 6) var3) (* (- 6) var2)) (- 10)) (>= (+ (* 6 var3) (* 6 var2)) 5)) (>= (+ (* (- 6) var3) (* (- 6) var2)) (- 2)))) (= A (store (store var4 1 var0) 1 (store (store (select var4 1) var5 var1) 2 0)))) (= (select (select var4 1) var5) 0))))))))) (not (= B true)))) )
However replacing the declaration of pl24 with the given definition gives an UNSAT formula.
pl24
The text was updated successfully, but these errors were encountered:
No branches or pull requests
Hello everyone,
it seems that eldarica returns an invalid model for the following code:
If I call
~/eldarica/eld -ssol test.smt2
I getHowever replacing the declaration of
pl24
with the given definition gives an UNSAT formula.The text was updated successfully, but these errors were encountered: