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
[180] % z3debug small.smt2 ASSERTION VIOLATION File: ../src/util/vector.h Line: 369 idx < size() (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB A [180] % cat small.smt2 (declare-fun |b@16| () (_ BitVec 32)) (declare-fun |c@93| () (_ BitVec 8)) (declare-fun |c@94| () (_ BitVec 8)) (declare-fun |c@95| () (_ BitVec 8)) (declare-fun |b@92| () (_ BitVec 32)) (declare-fun |b@168| () (_ BitVec 32)) (declare-fun |b@1240| () (_ BitVec 32)) (declare-fun |b@33608| () (_ BitVec 32)) (assert (or (and (bvule (bvadd |b@168| #b00000111111111111111111111111111) |b@33608|) (bvult (bvadd #b00000000000000000011111100000000 (bvmul |b@33608| (_ bv4294967295 32))) #b00000000000000000000000000011111) (bvule (bvadd |b@16| #b00000000000000000000000000001010 (bvmul (_ bv4294967295 32) (bvadd |b@168| (_ bv1 32)))) |b@1240|) (bvule |b@1240| |b@92|) (= |b@92| (bvor ((_ zero_extend 24) |c@94|) (bvshl ((_ zero_extend 24) |c@94|) (_ bv8 32)))) (= |b@1240| (bvor ((_ zero_extend 24) |c@94|) (bvshl (bvor ((_ zero_extend 24) |c@95|) (bvshl (bvshl ((_ zero_extend 24) |c@93|) (_ bv1 32)) #b00000000000000000000000000000010)) (_ bv8 32)))) (bvuge #b00000000000000001000000000000000 (bvadd |b@33608| (bvmul #b00000000000000111111111111111111 |b@1240|))) (bvuge |b@92| ((_ zero_extend 24) |c@95|)) (bvuge (_ bv81900 32) |b@16|)))) (check-sat) [181] %
Commit: 6c9bdc9
The text was updated successfully, but these errors were encountered:
982da8d
No branches or pull requests
Commit: 6c9bdc9
The text was updated successfully, but these errors were encountered: