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
Hi @wintersteiger!
The following test regressed with commit 9d57bdd It gives sat now, and it used to be unsat (which I believe was correct).
(declare-fun undef!10 () (_ BitVec 32)) (declare-fun |#exists!21| () (_ BitVec 2)) (declare-fun |#exists!19| () Bool) (declare-fun |#exists!18| () (_ BitVec 32)) (declare-fun |#exists!20| () Bool) (assert (forall ((undef!0 (_ BitVec 32)) (undef!1 (_ BitVec 32)) (undef!2 (_ BitVec 32)) (undef!3 (_ BitVec 32)) (choice!8 (_ BitVec 2))) (! (let ((a!1 (ite (and |#exists!20| (= ((_ extract 30 0) |#exists!18|) #b0000000000000000000000000000000)) (concat (bvnot ((_ extract 31 31) |#exists!18|)) ((_ extract 30 0) |#exists!18|)) |#exists!18|)) (a!2 (ite (= |#exists!21| #b10) (fp.isNaN ((_ to_fp 8 24) (ite |#exists!19| #x80000000 #x00000000))) (= |#exists!21| #b11))) (a!3 (ite (= ((_ extract 30 0) undef!1) #b0000000000000000000000000000000) (concat (bvnot ((_ extract 31 31) undef!1)) ((_ extract 30 0) undef!1)) undef!1)) (a!4 (or (= choice!8 #b01) (and (not (= choice!8 #b10)) (= choice!8 #b11)))) (a!8 (ite (and (= ((_ extract 30 0) undef!10) #b0000000000000000000000000000000)) (concat (bvnot ((_ extract 31 31) undef!10)) ((_ extract 30 0) undef!10)) undef!10)) (a!15 (fp.isNaN (fp.add roundNearestTiesToEven (_ -zero 8 24) (fp.neg ((_ to_fp 8 24) undef!1))))) (a!18 (fp.isNaN (fp.add roundNearestTiesToEven (_ +zero 8 24) (fp.neg ((_ to_fp 8 24) undef!1)))))) (let ((a!5 (not (ite (= choice!8 #b00) (fp.isNaN ((_ to_fp 8 24) a!3)) a!4))) (a!6 (fp.isNaN (fp.add roundNearestTiesToEven (_ -zero 8 24) (fp.neg ((_ to_fp 8 24) a!3))))) (a!9 (not (fp.isNaN ((_ to_fp 8 24) a!8)))) (a!11 (fp.isNaN (fp.add roundNearestTiesToEven (_ +zero 8 24) (fp.neg ((_ to_fp 8 24) a!3))))) (a!14 (not (ite (= choice!8 #b00) (fp.isNaN ((_ to_fp 8 24) undef!1)) a!4))) (a!16 (and (not (fp.isNaN ((_ to_fp 8 24) undef!1))) (not a!15))) (a!19 (and (not (fp.isNaN ((_ to_fp 8 24) undef!1))) (not a!18)))) (let ((a!7 (and (not (fp.isNaN ((_ to_fp 8 24) a!3))) (not a!6))) (a!12 (and (not (fp.isNaN ((_ to_fp 8 24) a!3))) (not a!11))) (a!17 (or a!14 (not (or (not a!16) a!9)))) (a!20 (or a!14 (not (or (not a!19) a!9))))) (let ((a!10 (or a!5 (not (or (not a!7) a!9)))) (a!13 (or a!5 (not (or (not a!12) a!9))))) (and (ite (= |#exists!21| #b00) (fp.isNaN ((_ to_fp 8 24) a!1)) (or (= |#exists!21| #b01) a!2)) a!10 a!13 a!17 a!20)))))))) (check-sat)
The text was updated successfully, but these errors were encountered:
Yeah, looks like I was a bit too aggressive with the NaN encodings in the theory solver, sorry for the inconvenience!
Sorry, something went wrong.
Successfully merging a pull request may close this issue.
Hi @wintersteiger!
The following test regressed with commit 9d57bdd
It gives sat now, and it used to be unsat (which I believe was correct).
The text was updated successfully, but these errors were encountered: