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
Assertion violation at ../src/smt/smt_conflict_resolution.cpp Line: 1259
[883] % z3debug small.smt2 ASSERTION VIOLATION File: ../src/smt/smt_conflict_resolution.cpp Line: 1259 conflict.get_kind() != b_justification::AXIOM (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [884] % [884] % cat small.smt2 (set-option :proof true) (set-option :smt.phase_selection 5) (declare-fun a () Int) (declare-fun b () Int) (declare-fun c (Int) Bool) (assert (= 0 (ite true (ite (c 0) 1 0) 0))) (assert (= b (ite (= a 0) (+ b 1) b))) (check-sat) [885] %
Commit: 4db41c0
The text was updated successfully, but these errors were encountered:
Assertion violation at ../src/ast/ast.h Line: 717
[891] % z3debug small.smt2 ASSERTION VIOLATION File: ../src/ast/ast.h Line: 717 idx < m_num_args (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [892] % [892] % cat small.smt2 (set-option :smt.dack.eq true) (set-option :smt.clause_proof true) (set-option :proof true) (declare-datatypes ((b!11 0) (e! 0) (j!7 0)) (((i(! e!))) (f (g(! e!))) ((l!5 (a!2 b!11) (k j!7)) m!6))) (declare-fun h!12 () j!7) (declare-fun c!3 (j!7) j!7) (assert (forall ((d!9 j!7)) (= (! d!9) (ite ((_ is m!6) d!9) m!6 (ite ((_ is l!5) d!9) (l!5 (! (a!2 d!9)) (c!3 (! d!9))) h!12))))) (check-sat) [893] %
Sorry, something went wrong.
Assertion violation at ../src/smt/dyn_ack.cpp Line: 60
[906] % z3debug small.smt2 ASSERTION VIOLATION File: ../src/smt/dyn_ack.cpp Line: 60 m.is_eq(eq) (C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB a [907] % [907] % cat small.smt2 (set-option :smt.clause_proof true) (set-option :smt.random_seed 2) (set-option :proof true) (declare-datatypes ((k 0)) (((h (a k)) (b)))) (declare-datatypes ((Lst 0)) (((cons (c k) (i Lst)) (nil)))) (declare-fun d (k k) k) (declare-fun count (k Lst) k) (assert (exists ((n k) (e k)) (distinct (d (h n) e) (h e)))) (assert (forall ((f k) (l k) (j Lst)) (= (count f (cons l j)) (ite (distinct f l) (h (count f j)) (count f j))))) (assert (forall ((n k) (f k) (g Lst)) (distinct (d (h b) (count n g)) (count n (cons f g))))) (check-sat) [908] %
c36355c
No branches or pull requests
Assertion violation at ../src/smt/smt_conflict_resolution.cpp Line: 1259
Commit: 4db41c0
The text was updated successfully, but these errors were encountered: