[Consolidated] issues with tactic.default_tactic=smt sat.euf=true #5417

rainoftime · 2021-07-18T12:22:55Z

Hi, for the following formula

(assert (> (/ 0 0.0) 1))
(check-sat-using qfufbv_ackr)

z3 cde3eac src/sat/smt/arith_solver.cpp:594

ASSERTION VIOLATION
File: ../src/sat/smt/arith_solver.cpp
Line: 594
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

NSB: this doesn't repro for me

The text was updated successfully, but these errors were encountered:

rainoftime · 2021-07-18T12:24:15Z

src/sat/smt/q_eval.cpp:243

(assert (forall ((s (_ BitVec 2))) (= s (ite (= (_ bv1 1) ((_ extract 1 1) s)) (_ bv0 2) (bvneg s)))))
(check-sat-using (then nnf aufnira))

z3 cde3eac

File: ../src/sat/smt/q_eval.cpp
Line: 243
l_false == compare(n, binding, s, t)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

rainoftime · 2021-07-18T12:26:16Z

src/util/vector.h:474

(declare-fun _substvar_555_ () (_ BitVec 32))
(declare-fun _substvar_545_ () (_ BitVec 2))
(assert (forall ((_substvar_1436_ (_ BitVec 1))) (exists ((_substvar_535_ (_ BitVec 1))) (forall ((_substvar_965_ (_ BitVec 1))) (and (= _substvar_965_ (_ bv1 1)) (= _substvar_545_ ((_ zero_extend 1) (bvcomp (_ bv0 32) (bvand _substvar_555_ #b00000000000000000000000000001001)))))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/util/vector.h
Line: 474
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

rainoftime · 2021-07-18T12:31:59Z

src/sat/smt/euf_invariant.cpp:59

(declare-datatypes ((Nat!1878 0)) (((zero!1881) (succ!1879 (pred!1880 Nat!1878)))))
(declare-datatypes ((Lst!1882 0)) (((nil!1886) (cons!1883 (head!1884 Nat!1878) (tail!1885 Lst!1882)))))
(declare-fun count!263 (Nat!1878 Lst!1882) Nat!1878)
(declare-fun error_value!1888 () Nat!1878)
(declare-fun l3 () Bool)
(assert (forall ((n!261 Nat!1878) (l!262 Lst!1882)) (= (count!263 n!261 l!262) (ite ((_ is cons!1883) l!262) (ite (= n!261 (head!1884 l!262)) (succ!1879 (count!263 n!261 (tail!1885 l!262))) (count!263 n!261 (tail!1885 l!262))) error_value!1888))))
(assert (= l3 (forall ((x!319 Nat!1878) (l!320 Lst!1882)) (= (count!263 x!319 l!320) (count!263 x!319 (cons!1883 x!319 l!320))))))
(check-sat-using (then purify-arith uflra))

ASSERTION VIOLATION
File: ../src/sat/smt/euf_invariant.cpp
Line: 59
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

rainoftime · 2021-07-18T12:41:05Z

AddressSanitizer: SEGV /src/ast/euf/euf_enode.h:154

(declare-datatypes ((Option!3 0)) (((None!1) (Some!1 (v!18 Int)))))
(declare-datatypes ((Method!1 0)) (((Method!2 (initials!1 (Array Option!3 Int))))))
(declare-fun d!5 () Bool)
(declare-fun isValidStep!1 ((Array Int Method!1) (Array Int Option!3) (Array Int Option!3) Int Int Option!3) Bool)
(assert (exists ((control!1 (Array Int Option!3))) (forall ((next_control!0 (Array Int Option!3))) (forall ((d!3 Bool)) (forall ((lambda!2 (Array Int Method!1))) (and (isValidStep!1 lambda!2 control!1 next_control!0 0 0 (Some!1 0)) (or d!3 (= control!1 ((as const (Array Int Option!3)) None!1))) (= next_control!0 (store ((as const (Array Int Option!3)) None!1) 0 (Some!1 0))) (or d!5 (= (isValidStep!1 lambda!2 control!1 next_control!0 0 0 (Some!1 0)) (= next_control!0 (store control!1 0 (Some!1 (select (initials!1 (lambda!2 0)) (Some!1 0)))))))))))))
(check-sat)

rainoftime · 2021-07-18T12:44:35Z

/src/sat/sat_solver.cpp:2539

(set-option :sat.branching.heuristic chb)
(declare-datatypes ((Nat!910 0)) (((Zero!913) (Succ!911 (x!912 Nat!910)))))
(declare-fun plus!207 (Nat!910 Nat!910) Nat!910)
(assert (forall ((x!205 Nat!910) (y!206 Nat!910)) (and (not (= y!206 (Succ!911 (plus!207 (x!912 x!205) y!206)))))))
(assert (forall ((x!210 Nat!910)) (or (not (= x!210 (plus!207 x!210 Zero!913))) (= (x!912 x!210) (plus!207 (x!912 x!210) Zero!913)))))
(check-sat)

rainoftime · 2021-07-18T12:47:03Z

src/math/simplex/model_based_opt.cpp:193

(assert (forall ((t48uscore0 Real)) (exists ((ep Real)) (forall ((ts48uscore0 Real)) (not (let (($x164 (and (>= ts48uscore0 t48uscore0) (not (= ts48uscore0 ep)))))))))))
(check-sat)

rainoftime · 2021-07-18T12:54:36Z

src/math/simplex/model_based_opt.cpp:192

(declare-fun yuscore2dollarskuscore23 () Real)
(assert (forall ((t13uscore0dollarskuscore0 Real)) (not (exists ((ts13uscore0 Real)) (or (< yuscore2dollarskuscore23 1) (and (> ts13uscore0 t13uscore0dollarskuscore0) (not (= 1 (+ 1.0 ts13uscore0)))))))))
(check-sat)

rainoftime · 2021-07-18T13:15:06Z

src/sat/smt/q_eval.cpp:212

(declare-sort node$type)
(declare-datatypes ((cache_state$type 0)) (((invalid) (shared) (exclusive))))
(declare-datatypes ((cache$type 0)) (((c_cache$type (c_state cache_state$type)))))
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-fun cache () (Array node$type cache$type))
(declare-fun recv_invack$i () node$type)
(declare-fun shrset () (Array node$type BOOL))
(declare-fun shrset$1 () (Array node$type BOOL))
(assert (let (($x66 (or (or (and (forall ((n node$type)) (= Truth (select shrset n))) (forall ((n node$type)) (let (($x10 (= exclusive (c_state (select cache n)))))))) true (= shrset$1 (store shrset recv_invack$i Falsity))) (= Truth (ite true Truth (ite (forall ((n node$type)) false) Truth Falsity))))))))
(assert (let (($x152 (forall ((n node$type)) (or (= Truth (select shrset n)) (not (= invalid (c_state (select cache n))))))))))
(assert (not (= Truth (ite false Falsity (ite false Truth Falsity)))))
(check-sat)

rainoftime · 2021-07-18T13:30:12Z

src/sat/smt/euf_solver.cpp:369

(set-option :rewriter.elim_and true)
(declare-fun _substvar_4583_ () (Array (Array Bool (Array (Array (Array Int (Array Real Real)) (Array Real (Array Real Real))) (Array (Array (Array (Array (Array (Array Real Real) Real) Real) Bool) (Array (Array (Array (Array (Array Real Real) Int) (Array (Array (Array (Array Real Real) Int) (Array (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real Real)) (Array Int (Array Real (Array (Array Real Real) Real)))) (Array (Array Real Real) Int))) Bool)) (Array (Array (Array (Array Real Real) Real) Real) Bool)) (Array (Array Real Real) (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real (Array (Array Real Real) Real))) (Array Int (Array Real (Array (Array Real Real) Real))))))) (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real (Array Real Real))) (Array (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real Real)) (Array Int (Array Real (Array (Array Real Real) Real)))) (Array (Array Real Real) Int)))))) (Array (Array (Array (Array Real Real) Int) (Array (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real Real)) (Array Int (Array Real (Array (Array Real Real) Real)))) (Array (Array Real Real) Int))) Bool)))
(assert (forall ((_substvar_4177_ Bool)) (exists ((_substvar_2673_ Bool)) (forall ((aaa (Array (Array Bool (Array (Array (Array Int (Array Real Real)) (Array Real (Array Real Real))) (Array (Array (Array (Array (Array (Array Real Real) Real) Real) Bool) (Array (Array (Array (Array (Array Real Real) Int) (Array (Array (Array (Array Real Real) Int) (Array (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real Real)) (Array Int (Array Real (Array (Array Real Real) Real)))) (Array (Array Real Real) Int))) Bool)) (Array (Array (Array (Array Real Real) Real) Real) Bool)) (Array (Array Real Real) (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real (Array (Array Real Real) Real))) (Array Int (Array Real (Array (Array Real Real) Real))))))) (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real (Array Real Real))) (Array (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real Real)) (Array Int (Array Real (Array (Array Real Real) Real)))) (Array (Array Real Real) Int)))))) (Array (Array (Array (Array Real Real) Int) (Array (Array (Array (Array Real (Array (Array Real Real) Real)) (Array Real Real)) (Array Int (Array Real (Array (Array Real Real) Real)))) (Array (Array Real Real) Int))) Bool)))) (and _substvar_2673_ (= aaa _substvar_4583_) (= _substvar_4583_ aaa))))))
(check-sat)

rainoftime · 2021-07-18T13:36:10Z

src/sat/smt/q_eval.cpp:158

(declare-datatypes ((cache_state$type 0)) (((invalid) (shared) (exclusive))))
(declare-datatypes ((msg_cmd$type 0)) (((reqs) (gnts))))
(declare-sort data$type)
(declare-datatypes ((msg$type 0)) (((c_msg$type (m_cmd msg_cmd$type) (m_data data$type)))))
(declare-datatypes ((cache$type 0)) (((c_cache$type (c_state cache_state$type) (c_data data$type)))))
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))
(declare-sort node$type)
(declare-fun shrset () (Array node$type BOOL))
(declare-fun exgntd () BOOL)
(declare-fun send_invack$i () node$type)
(declare-fun cache () (Array node$type cache$type))
(declare-fun cache$1 () (Array node$type cache$type))
(declare-fun chan3$2 () (Array node$type msg$type))
(declare-fun l3 () Bool)
(assert (= (ite l3 (ite (or true) Truth Falsity) (ite (or (forall ((n node$type)) (or (not (= exgntd Truth)) (= (select shrset n) (ite (= n send_invack$i) Truth Falsity)))) (not (= chan3$2 (store chan3$2 send_invack$i (c_msg$type (m_cmd (select chan3$2 send_invack$i)) (c_data (select cache send_invack$i)))))) (= cache$1 (store cache$1 send_invack$i (c_cache$type invalid (c_data (select cache send_invack$i)))))) Truth Falsity)) Truth))
(check-sat)

rainoftime · 2021-07-18T13:40:07Z

heap-use-after-free at vector.h:401

(set-option :rewriter.arith_ineq_lhs true)
(declare-fun x1 () Real)
(assert (forall ((x0 Real)) (and (= 1 (+ (* x0 (- 2)) (* x1 (- 36)))) (= 1 (- (* x0 (- 4)) x1 (* x0 (- 40)))) (or true))))
(check-sat-using smt)

NB. Might still be there. I don't have UBSAN handy ATM.

rainoftime · 2021-07-18T13:53:15Z

src/sat/smt/euf_model.cpp:217

(set-option :smt.ematching false)
(declare-datatypes ((a 0)))
(assert (forall ((e (Seq a))) (not (= 0 (seq.len (seq.extract (seq.++ (seq.unit false) (seq.unit true)) 1 (- 1 (seq.len (ite (= 0 (seq.len e)) (as seq.empty (Seq Bool)) (seq.unit false))))))))))
(check-sat-using (then simplify nnf ufbv))

NB: sequences are not part of sat.euf yet

rainoftime · 2021-07-18T13:54:35Z

heap-use-after-free src/sat/smt/q_mam.cpp:2747

(declare-sort worlds)
(declare-fun val (worlds worlds) Bool)
(declare-fun v!1 () worlds)
(declare-fun access (worlds worlds) Bool)
(assert (exists ((w!1 worlds)) (forall ((g worlds)) (and (access w!1 v!1) (forall ((w worlds)) (exists ((v worlds)) (and (val g v) (access w v)))) (forall ((x worlds) (y worlds) (z worlds)) (or (not (access x y)) (not (val x z)) (access y z)))))))
(check-sat)

rainoftime · 2021-07-18T14:08:17Z

src/sat/smt/sat_dual_solver.cpp:130

(assert (exists ((r3 Real)) (forall ((v4 Bool)) (exists ((v2 Bool)) (and v2 v4 (or (< 1.0 r3) (< r3 0.0)))))))
(check-sat)

rainoftime · 2021-07-18T15:03:21Z

src/sat/smt/q_ematch.cpp:340

(declare-fun a (Bool Bool Int Int Int Int Int Int Int) Bool)
(assert (and (forall ((bc Bool) (bd Bool) (bf Int) (bm Int) (bn Int) (bk Int) (b Int) (e Int) (gd Bool)) (not (a bc bd bf b bm bn bk e b))) (forall ((b Int) (bc Bool) (bd Bool) (bk Int) (be Int) (bf Int) (bm Int) (bn Int)) (or (not (= bd false)) (a bc bd bf b bm bn bk be b)))))
(check-sat)

NikolajBjorner · 2021-07-18T17:07:39Z

OK, thanks.

#5417 (comment)

…ncies with post-hoc explain function

mam assumes the egraph isn't updated during callbacks.

strict inequality (over reals) require solving for least-upper/greatest-lower bounds that may coincide with non-strict inequalities (be epsilon stronger). Instead of using the coefficient 'a' to turn the inequality into an equality, add the slack value as a constant.

more gracefully handle non-implemented theories

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner · 2021-07-19T22:38:07Z

Likely #5417 (comment) remains, but I don't have an easy way to observe it.

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

@agurfinkel

* Update z3 from branch 'master' to 3c18fc367058950f81fb9c40041012345c42ef65 - V125-012 Merging z3 4.8.14 into Adacore master Change-Id: Icd62ac968009230b5cdd6dbdea3068339d5a21f3 - Update release.yml for Azure Pipelines - Update release.yml for Azure Pipelines - Update release.yml for Azure Pipelines - update release scripts and notes in master Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - improved subset checking for regexes with counters (#5731) - #5722 - internalize unary xnor - wrong unit for xor in aig tactic #5722 - Migrate from deprecated `distutils.sysconfig` in scripts (#5729) - remove action that fails too often - Use Stdlib. instead of Pervasives. due to deprecation (#5730) - bug in flatten/and/or introduced when skipping sub-expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - update comment Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix deadlock in scoped_timer destructor (#5371) - fix a few compiler warnings - improved regex merging avoiding unsat nontermination (#5728) - fix c++ Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5727 Expose diff function, expose allchar in Java API expose op codes for replace/re/all - fix again - Merge branch 'master' of https://github.com/z3prover/z3 - fix #5726 - fixed bug in is_char_const_range (#5724) - fixing regression of issue 1224 (#5723) - na - Update z3++.h simplify definition - State graph dgml update and fixes in condition simplifier (#5721) * improved generated dgml graph * fixed simplification of negated ranges and did some code cleanup * do not make loops with lower=upper=0, this is epsilon * do not add loops with lower=upper=1 * bug fix in normalization: forgotten eps case - na - na - Update z3++.h with bindings for user propagate functions - move user propagte declare to context level declaration of user propagate functions are declared at context level instead of at solver scope. - na - expose propagate created - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - adding a new toy for Clemens Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na - fixes to previous push and streamlining - pin expressions - prepare user propagator declared functions for likely Clemens use case - Update regex union and intersection to maintain ANF (#5717) * added merge for unions and intersections * added normalization rules to ensure ANF * fixing PR comments related to merge - Update nightly.yaml see if this gets us past the upload to GitHub issue - #5700 - Add download x86 as part of release NuGet x86 is part of nightly NuGet but was not added to the release pipeline. - fix #5710 - fix #5714 It is not unlike other fuzz bugs: it exercises some behavior that applications are unlikely to expose. In this case, a rule body expanded into a conjunction with more than 1M formulas (with a lot of repetition). The original rule representation assumed silently that the number of constraints in a body would fit within 20 bits, but reality allowed bodies with as many as 2^{32} - 1 constraints. So "minimizing" the bug as @agurfinkel asks for seems not to make too much sense. Just running the samples in debug mode points to the root cause. Since fuzz bugs are not from applications and fuzz tools have the potential for creating a large number of issues, I find it reasonable to push some basic pro-active asks on filers: - reproduce bug in debug builds to assess whether a debug assert triggers. - minimize or keep it simpler when possible (in this case it does not apply) - perform basic diagnostics/triage. I am basically asking to push this part of the work on to the fuzzer. Otherwise, addressing random bugs doesn't scale. Triaging should have pointed to the root cause. Now, there tends to be something to learn from bugs. In this case, the question was: "can we avoid constraints with duplications"? In particular, it points to a basic inefficiency of extracting conjunctions (and disjunctions). The function didn't deduplicate. So I added deduplication into this function. It is used throughout z3 code base so could expose latent issues. We will see. - fix #5715 - remove EnumToNative as it drops reference counts, fixes #5713 - Cleanup regex info and some fixes in Derivative code (#5709) * removed unused regex info fields * cleanup of info and fixes in antimirov derivatives * removed extra qualification on operator - remove dead code - na - fix co-factoring' Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix co-factoring Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - remove case for non-emptiness to combine with standard membership as part of revising engine for addressing #5693 - stdout Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - hoisting out blocker for empty #5693 - include atomic Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5704 - this one is for you Nuno - pull request might have new bugs given that build is broken. - this test doesn't expose race conditions under simple tests, yet. It is a starting point. - run under cuzz (app-verifier) should expose races, this is what it was made for. - add stub for testing updates to scoped_timer Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Fix return type of as_int64 (#5703) - fix spelling - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - unsound equality propagation #5676 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - replace_re axiom placeholder @ahelwer - illustrates placeholder for one approach for axiomatizing replace_re - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add tactic name Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - pass through for unary tactical - add ability to register expressions during callback - register forbidden functions with reduce_args for user-propagator - clear tactic user propagate state on solver destructor - update arithmetic contract for unbounded (#5696) Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - start using lar_solver::is_feasible() (#5697) Signed-off-by: Lev Nachmanson <levnach@hotmail.com> - Handle correctly cancelled run (#5695) * remove the bound on total iterations in simplex Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove unncesseray checks in get_freedom_interval_for_column() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix the build of test-z3 Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Revert "remove unncesseray checks in get_freedom_interval_for_column()" This reverts commit 6770ed85e3a09c2f0373464d77305438522a03cb. * optimize get_freedom_interval_for_column() for feasible case Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add function lar_solver::status_feasible Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename status_is_feasible() to is_feasible() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix the linux build Signed-off-by: Lev Nachmanson <levnach@hotmail.com> - remove - fix bug in smt_tactic_core for translating user-ids - update input for doxygen #5400 - fix translation for equality propagation - prevent stale user-propagators from being used on the same tactic after it was applied. - don't rely on cleanup - typo - indirection for user ids - only use setup_and_check if there is no user propagator set. - adding checks Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - infeas Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - try delay init for user propagator in smt_tactic Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - stack Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - enable user propagation on tactics Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - three smt2 examples added and one python example updated (#5690) - fix regression from today, see #5676 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5687 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - try th_lemma, update documentation of api functions for creating strings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - change user propagation to apply scheme similar to theory_recfun Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fixing #5473 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add virtual destructor Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - base -> core - rename files to theory_user_propagator - introducing base namespace for user propagator - add debug information in user-propagate #5687 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5641 - remove an unused var Signed-off-by: Lev Nachmanson <levnach@hotmail.com> - #5641 - fix #5681 - fix #5679 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - include thread Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - wasm build issue Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Merge branch 'master' of https://github.com/z3prover/z3 - ensure smt2log works with multi-threaded consumers, ease scenarios around #5655 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5675 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - revert use of f format Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - mac builds Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5674 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - if you read this commit message you probably are a programmer who has no life Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Update release.yml for Azure Pipelines - Update release.yml for Azure Pipelines - Update release.yml for Azure Pipelines - update release pipeline Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - enable publish Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - update release notes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Fix stray semicolon in examples (#5669) - nightly Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - update nightly Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - prepare release Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5663 - check for v1 == v2 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5614 turn on / off options to get better performance. Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5653 fix performance bottleneck in static features - add EFSMT solving example (#5654) Co-authored-by: rainoftime <rainoftime@gmail.com> - fixing issues with user propagator from python "fresh" remains broken (not working yet). - capture values not reference - #5646 - #5643 - Added user propagator example (#5625) * Added user propagator example * User propagator example code refactoring (+ removed unused parameter warning) * Moved user-propagator example to its own directory - working on #5614 there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately: - m_bv_to_propagate is too expensive - lp_bound_propagator misses equalities in two different ways: - it resets row checks after backtracking even though they could still propagate - it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable. FYI @levnach - build warnings - ubuntu 16 is no more Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Update wasm.yml - Update README.md - Update wasm.yml - Update wasm.yml - Update wasm.yml - Update wasm.yml - Update wasm.yml - Use emscripten to create a wasm build (#5634) - Update azure-pipelines.yml make it green - Add and fix a few general compiler warnings. (#5628) * rewriter: fix unused variable warnings * cmake: make missing non-virtual dtors error * treewide: add missing virtual destructors * cmake: add a few more checks * api: add missing virtual destructor to user_propagator_base * examples: compile cpp example with compiler warnings * model: fix unused variable warnings * rewriter: fix logical-op-parentheses warnings * sat: fix unused variable warnings * smt: fix unused variable warnings - fix one typo and two misunderstandings for doxygen (#5633) - fix misspelled \brief for doxygen (#5632) - Create wasm.yml initial wasm - fix performance regression after adding user declared functions to model Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix grouping for latest doxygen (#5626) Since doxygen 1.8.16, opening and closing a group must not be done as C comment but as doxygen command. In other words, not one but two asterisk characters are required so that doxygen finds a group. - Fix the command of `install_name_tool -id`. (#5622) * Fix the command of `install_name_tool -id`. * Fix: don't call `ml_example.byte`. - ex handler Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #4869 load datatype parsing for HORN logic Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add ref for regression Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - strengthen contract for log_axiom_instantiation #5621 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - strengthen contract for log_axiom_instantiation #5621 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fixed nullability bug in the if-then-else info (#5620) - update build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - try get_string contents again Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - update API type annotation to make it OCaml friendly - support threading for TRACE mode - Update azure-pipelines.yml for Azure Pipelines - Update azure-pipelines.yml for Azure Pipelines - Update azure-pipelines.yml for Azure Pipelines - Fix ocaml link and load (#5618) * Add path flags for cc loader (linux). * Fix os linking and loading problem (maybe on #4840). - Add post-install testing for ocaml binding. (#5617) * Add path flags for cc loader (linux). * Fix os linking and loading problem (maybe on #4840). * Add post-install test of OCaml binding on ubuntu. * Minor. * Tentative CI for macos. - #5615 - update documentation and use non-encoded versions for ASCII characters in get_lstring Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - use some suggestions from #5615 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - remove deprecated escape string from Julia bindings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Fix runtime search path for shared-lib and add '-static' to the name of static-lib. (#5616) * Fix runtime search path for shared-lib and add '-static' to static-lib. * Revert the change on `META.in`. - updated C++ API for escaped and unescaped strings #5615 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add API to access unescaped strings, update documentation of Z3_get_lstring, #5615 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - print bounded terms for better efficiency - add handling of quantifiers #5612 - Merge branch 'master' of https://github.com/z3prover/z3 - #5605 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5605 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Added eq/fixed/final functions in C++ user propagator as methods (#5607) - push-pop Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add nff and auto-relevant Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5604 retain array interpretation when available - fixes to sat.euf ematching #5573 - fixed bug of computing butlast of a sequence (#5602) - updated printer - Regex range bug fix (#5601) * added a missing derivative case for nonground range * further missing cases and a bug fix in re.to_str - tweak GC in OCaml bindings (#5600) * feat(api/ml): use custom block hints to guide the GC this forces the GC to collect garbage when a few _large_ objects (solver, etc.) are dead. The current code would let arbitrarily many such objects die and not trigger a GC (which would have to come from OCaml code instead) * tuning * try to use caml_alloc_custom_mem with fake sizes * try to fix leak by explicitly finalizing OCaml context * chore: use more recent ubuntu for azure CI * remove finalizer causing segfault in example - #5591 - #5593 - fix #5594 - Update smt_context.cpp - fix #4901 - #5591 nth issue - Merge pull request #5550 from wintersteiger/cwinter_fpa_fixes Assorted fixes for floats - #5467 - Revert "Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it." This reverts commit f80fdb4ea3a762cfe95daa0321d9875cfa00c7ae. - Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it. - Fix for mk_to_fp_float; pertains to #4841 - Make terms that are internalized on the fly relevant - Add additional equality in theory_fpa - Make fpa2bv debug symbol names optional - Whitespace - Refine fpa_decl_plugin::is_unique_value - Fix error messsages - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5589 - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Update README.md - Create android-build.yml (#5588) - fix max/min length to handle concatenation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Rename 'user' to 'user_solver' #5586 (#5587) Issue #5586 reported that Android builds (targetting, e.g., x86) failed to compile due to a conflict between: * `struct user` in `sys/user.h`; and * `namespace user` in z3's `user_solver.h` This issue is resolved by renaming `namespace user` to `namespace user_solver` (matching the header name) to avoid this conflict. Reported-by: Jamie Collinson <jamiecollinson@gmail.com> Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com> - fix internalize regression Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Newderiv (#5585) * updated derivative engine * some edit * further improvements in derivative code * more deriv code edits and re::to_str update * optimized mk_deriv_accept * fixed PR comments * small syntax fix * updated some simplifications * bugfix:forgot to_re before reverse * fixed PR comments * more PR comment fixes * more PR comment fixes * forgot to delete * deleting unused definition * fixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Margus Veanes <margus@microsoft.com> - Updated regex derivative engine (#5567) * updated derivative engine * some edit * further improvements in derivative code * more deriv code edits and re::to_str update * optimized mk_deriv_accept * fixed PR comments * small syntax fix * updated some simplifications * bugfix:forgot to_re before reverse * fixed PR comments * more PR comment fixes * more PR comment fixes * forgot to delete * deleting unused definition * fixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fixes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> - disable all propagation until ematch incompleteness is fixed Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - remove arith_lhs simplification from preamble tactic Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - redo bindings/fingerprints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - unit propagate with fingerprints - fix #5579 - It is only possible to reach this case when new assertions are created. - missing continue fixes unsound sat result from #5573 - Update z3++.h - disable macro finder tactic if there are recursive functions fix #5574 - fix tmp_eq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix tmp_eq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - tune q-eval and q-ematch Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - tuning eval - count lazy bindings - add extra commands to API parser - lifting iff to binary - Correct capitalization of package (#5569) See https://stackoverflow.com/a/50004273/1167061 - #5532 - #5532 - #5532 - import goodies from ps Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5545 - #5532 - #5532 - fix build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5541 - CNF conversion refactoring (#5547) * split sat2goal out of goal2sat These two classes need different things out of the sat::solver class, and separating them makes it easier to fiddle with their dependencies independently. I also fiddled with some headers to make it possible to include sat_solver_core.h instead of sat_solver.h. * limit solver_core methods to those needed by goal2sat And switch sat2goal and sat_tactic over to relying on the derived sat::solver class instead. There were no other uses of solver_core. I'm hoping this makes it feasible to reuse goal2sat's CNF conversion from places like the tseitin-cnf tactic, so they can be unified into a single implementation. - Fix Z3Config.cmake.in when generating a static library (#5555) - #4880 add interpreted versions of to_bv functions for MBQI quantifier models - ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fixes for model converter default case - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - prepare for min/max i Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - enforce idempotency bug reported by Clemens - Added character functions to API (#5549) * Added character functions to API * Changed names of c++ functions - #5546 try dampening - bv2char and char2bv with Clemens Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - make it easier to debug parallel - fix regression bug in mam reported by Aseem - Added 16 bit string-encoding (#5540) - handle potential extra nodes from q_solver - #5532 - #5532 add blocking condition for recursion. - left over bugs #5532 disabling complete const rewriting (temporarily) as it can loop - #5532 remove unsound rewrite rule that was recently added - #5532 bugs in: - rewriting of 0-ary expressions was incomplete - sharing annotations when a node has two theories attached it is shared - sharing of const of an array Remove unreadable part of pretty printer for lp solver. - #5532 ensure re-internalization for predicates that are replayed. Theory internalization is currently not considered in depth. - #5532 - #5532 - revisit as-array evaluation - const rewriting revisited - #5532 - handle null more gracefully - #5532 - modernize parameter defaults Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5532 remove "reflect" parameter from exposed options. It should be internal only. - #5532 - #5532 - #5532 - #5532 - #5532 - throw less #5519 - #5528 - make it easier to iterate over arguments of an application Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - merge Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Merge branch 'master' of https://github.com/z3prover/z3 - add extra checks that user-supplied assumptions are asserted Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - account for updating scoped state by goal2sat #5528 - #5528 - more useful diagnostics - follow on fix from #5528 the same bug is also undetected in the main solver - #5528 - #5528 - #5516 expose ability to expand select/store and select/ite (lambdas are always expanded) during pre-processing for N.P. Lopes. - build - add to_string method to make it easier to use without << - #5528 - fix #5526 when propagation claims progress, but is a no-op. - Update solver_subsumption_tactic.h use naming convention with - instead of _ for tactics - #5528 - round-tripping escapes, again #5519 - fix part of #5519 generation of escape sequences for output was not handling non-printable character ranges correctly and also not offsetting hexadecimal characters right. - #5518 patch a gaping hole in recfun - #5518 - #5518 @wintersteiger This example exposes a bug in is_unique_value ``` (assert (= (fp.to_real ((_ to_fp 8 24) (_ bv4286579200 32))) (fp.to_real ((_ to_fp 8 24) (_ bv4286578944 32))))) (check-sat) ``` It returns true for fp representations that map to NaN. It can only return true for fp values that are unique relative to having no other bit-vector representation so not corresponding to an equivalence class of values such as NaN. I am having it return false. If there is a way to refine the test it will catch some earlier inferences. - #5518 - #5518 - #5518 - #5518 regression from adding lambdas in model - fix the use of ctx in Q() (#5521) * fix #4956 * fix: use ctx in Q() - #5482 fix default case for model construction port mg_merge functionality from theory_array_base that ensures default values in arrays congruent modulo stores are the same - logging cleanup move everything out-of-line as common path doesn't log fix some race conditions on file ptr vs enable_logging vars - logging: don't call the returned function twice (one for log, one for return) Z3_simplify() does RETURN_Z3(simplify(...)), hence the function was being called twice it turns out simplify is not idempotent, so calling it twice can result in different results thus breaking the log. - fix logging in Z3_fpa_get_[es]bits - fix #5515 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - bail on first model validation failure Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - simplify based on comment from Jamie Sharp #5512 - fix logging of Z3_mk_lambda and Z3_mk_lambda_const In preparation of a bug report just for you @NikolajBjorner - Integrate fixes from #5512 Pull request #5512 identifies a in line 1139 where the const-case-multiplier constructor returns false and does useless work. In this update we also remove mk_const_multiplier because code path is subsumed by mk_const_case_multiplier. - #5482 remove overly permissive filter on select_store axiom - remove wtm and booth Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - bit_blaster unit tests for adder and multiplier (#5514) These tests cover a mix of constant and non-constant input bits. - handle constants Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add missing lambda defs per #5509 the result is now unknown because the nested expression contains exists, which doesn't get replaced by universal quantifier which is assumed by the legacy core. The legacy core should not depend on universal quantifiers only, but fixing this is a risk. Workaround is to rewrite goals using forall only (replace exists by de-Morgan dual). - #5507 can't use auto-config if there are no assertions. Auto-config only works properly for one-shot mode since theories aren't loaded on demand in this solver. - types Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - re-add API for creating propagator from a context for "fresh" - missing this Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5507 missing init - regressions from previous push - update Bool rewriter to pull negations up - extend macro detection to negated equivalences #5496 - missing rewrite exposed by #5498 - #5482 other relevancy tracking - don't copy "true" - #5482 - #5482 add unit propagation - #5482 - use datatype name instead of instantiation for cycle detection #5482 - #5482 non-termination (stack overflow) bug in recursive comparison - update project description #5503 - #5499 throw exception when dividing by a small 0 - #5482 update temp variables - char sort Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add character sort to Python API and allchar function to API for ease. #5500 - missing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5482 tricky one - #5497 - finally expose some easier to use basics could be used in cases such as #5496 - fix #5491 - remove likely culprit for #5493 @zwimer: I had to remove a different move constructor before in the same API due to a different bug that the coverage tool exposed. I was unable to reproduce the bug reported in #5493 in my environment, but the interaction with reference counting and move constructors is sufficiently opaque that I rather not have to fix more bugs introduced with move constructors in the API. I am therefore removing also this use of && and maybe this fixes #5493 - #5454 again Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - comment out for now - try without semi-colon - #5454 again - Update test for java - try vscode from github integration - move examples to python based build - fix regression in FPNumRef sign - #5488 - #5486 - improve type elaboration by epsilon to make common cases parse without type annotation - build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - expose method for updating python model for constants Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Update array_axioms.cpp - remove dependencies on stale component - Update coverage github action (#5483) * Correctly emits simple and detailed coverage reports using a combination of `gcovr` and `llvm-cov gcov` * Uploads the reports as associated artifacts, with 4 days of retention * Executes on every `master` push, and daily at 11 UTC Co-authored-by: Andrei Lascu <andrei.lascu10@imperial.ac.uk> - #5484 - modify #5454 - #5454 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5454 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5454 @wintersteiger: added code review comment to theory_fpa. The bug seen in #5454 doesn't surface with theory_fpa, though. - reorder fields - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - widen scope of der #5480 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - expose n-ary xor - Specify and document value for environment variable for loading native library in Java bindings (#5477) * limit range of environment variable for loading the native library in Java to "true". This change specifies the range of values that are allowed to set the environment variable "z3.skipLibraryLoad". Only the value "true" (in upper-, lower-, and mixed-case is accepted as valid value. Other values, such as "false", "0", "1", "foo", an empty or a missing value are evaluated to "false" and cause the default loading of the native library. * adding documentation about environment variable for (not) loading the native library in Java. This is a follow-up commit for #4667 to provide a publicly visible documentation. - Add AssertSoft String overload for Java Api (#5475) This adds a String overload for AssertSoft. Previously only integer weights could have been used, limiting the user. With Strings the user can now use e.g. Java's BigInteger class converted to a String instead. - #5454 - #5454 - #5454 - #5454 - #5454 - #5454 - #5454 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5454 - fix solver-subsumption again, #5468 (negation was swapped in original wrong subsumption check, then soundness fix removed core subsumption functionality) Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5454 - fix #5468 - lost update from August 3 #5468 - remove useless literal found during review #5470 - fix #5469 documentation bug - more fixes related to issue #5140 (#5466) * instead of u in to_re(s) make u = s * bug fix: added missing emptiness check - rewrite equality too Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix equality rewrite with itos Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - updates related to issue #5140 (#5463) * updates related to issue #5140 * updated/simplified some cases * fixing feedback comments * fixed comments and added missing case for get_re_head_tail_reversed * two bug fixes and some other code improvements - #5460 - #5460 NB @nunoplopes - the code path regarding rewrite_uncstr could use some unit tests. - #5460 - report which operator bit-blast failed on (#5459) - support bit-blasting bvand (#5458) - more rewrites based on example in #5457 - fix #5457 - #5454 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5456 - #5452 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - merge Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fix #5452 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Sharon & Neta notes Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5445 - #5445 - Correct a typo in contrib/ci/README.md (#5453) - #5445 - #5140 - format - format Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Update coverage.yml - Improve coverage CI script (#5451) * Due to the long duration of the CI execution, execute it at a set time daily (currently 11 UTC / 4 PDT) * Use `Ninja` to build instead of Makefile, due to better compilation time * Execute all the available Z3 tests and examples: `test-z3 -a`, `z3test` regression suites (`smt2`, `smt2-debug`, and `smt2-extra`), `z3test` coverage tests, and the 4 provided examples * Upload `gcovr` report as an artifact associated with the CI run TODOs: * Fix `gcovr` emitting an empty report * Potentially take the artifact and upload it somewhere accessible Co-authored-by: Andrei Lascu <andrei.lascu10@imperial.ac.uk> - #5445 - #5445 - #5447 That the bug went away is a fluke. It wasnt fixed. It is in pb-preprocess, an essentially unused tactic. The special subsumption resolution rule wasn't accounting for membership of all variables. - #5445 - fix #5449 - #5429 #5445 - #5429 again - fix #5446 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - remove sine filter #5446 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Update wip.yml - Update README.md - remove out Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add wip Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - remove coverage job from azure-pipeline as it is now in a self-contained action Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na - misc warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Update coverage.yml - Update coverage.yml - Update coverage.yml - Update coverage.yml - Update coverage.yml - Update coverage.yml - Update coverage.yml - Update coverage.yml - Update coverage.yml - Update coverage.yml - Update coverage.yml - fix regression in goal2sat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - cleanups Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Update README.md - Create coverage.yml Move coverage to self-contained github action - #5429 - use quantifier - flatten if-then-else - disable drat inside of quantifier elaboration - jobs Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - jobs Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - coverage.yml Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - build/labels - #5429 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5429 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5429 - #5429 - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - re-move #5442 - #5429 relevancy propagation applies to quantifier unfolding. - rename Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Merge branch 'master' of https://github.com/z3prover/z3 - add dummy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Add Ubuntu CMake Coverage CI step (#5442) Adds an extra step to CI jobs which executes the Z3 test suite with coverage enabled, and additionally executed coverage-enhancing tests added to z3test. - fix #5439 - Need `-thread` option to compile OCaml example (#5440) I can compile the OCaml example with `-thread` option at Linux. ``` $ ocaml --version The OCaml toplevel, version 4.05.0 ``` - #5429 - #5429 - proviso for different life-time of objects allocated in arguments. - err - fix #5435 - change debug output - fix #5430 - #5429 #5431 - simplify #5431 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - added derivative support for (str.to_re (str.from_int ...)) (#5431) - #5429 - #5425 Add an alternative to unit-subsume-simplify It is called solver-subsumption It does a little more than unit-subsume-simplify and also uses a different decomposition algorithm for clauses. It removes redundant constraints and simplifies clauses in a single pass. A possible use of this tactic is in isolation where the maximal number of conflicts (smt.conflicts_max, sat.conflicts_max) are bounded. For simpler formulas full solver calls may be still feasible. - sat.euf add missing function - fix #5424 - #5427 - #5427 - #5427 - #5427 - remove unused dependency - #5422 - #5422 - #5422 - #5422 - #5422 - avoid perf abyss for macros Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5420 - #5420 - #5420 - #5420 - #5420 - #5420 - #5417 again, refining root clauses above search level Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5331 - #5331 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5417 designate quantifier axioms as auxiliary Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - #5417 more gracefully handle non-implemented theories - #5417 - na - #5417 strict inequality (over reals) require solving for least-upper/greatest-lower bounds that may coincide with non-strict inequalities (be epsilon stronger). Instead of using the coefficient 'a' to turn the inequality into an equality, add the slack value as a constant. - #5417 extend definition of ground to be variable free - #5417 - delay propagation from callbacks from mam mam assumes the egraph isn't updated during callbacks. - #5417 normalize clause - #5417 - revise q_eval based on bug based on non-chronological dependencies with post-hoc explain function - #5417 Z3Prover/z3#5417 (comment) - #5417 - #5323 Z3Prover/z3#5323 (comment) - #5323 - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - Merge branch 'master' of https://github.com/z3prover/z3 - add consequences forcing character values to be digits - added regex simplification rules ~() = .+ and .+* = .* (#5416) - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add comments - note - #5336 missing theory variable creation in fpa_solver - #5336 - assertion violation in q_solver - Added sbv2s (#5413) * Added sbv2s * Fixed indention Co-authored-by: Clemens Eisenhofer <Clemens.Eisenhofer@tuwien.ac.at> - bound length of ubv2s Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - fixed bug #5343 and did some related optimizations (#5411) - remove incorrect and inefficient default model conversion - fix boundary cases reported by Clemens - charsort Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - add char sort to .net Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - na Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> - version inc, bvsort->bitvecsort - adding access to characters over API Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner added a commit that referenced this issue Jul 18, 2021

#5417

750c06e

NikolajBjorner added a commit that referenced this issue Jul 18, 2021

#5417

e8bc9f3

#5417 (comment)

NikolajBjorner added a commit that referenced this issue Jul 19, 2021

#5417 - revise q_eval based on bug based on non-chronological depende…

7d915eb

…ncies with post-hoc explain function

NikolajBjorner added a commit that referenced this issue Jul 19, 2021

#5417 normalize clause

776f270

NikolajBjorner added a commit that referenced this issue Jul 19, 2021

#5417 - delay propagation from callbacks from mam

3156ca5

mam assumes the egraph isn't updated during callbacks.

NikolajBjorner added a commit that referenced this issue Jul 19, 2021

#5417 extend definition of ground to be variable free

49b94a0

NikolajBjorner added a commit that referenced this issue Jul 19, 2021

#5417

0a34eef

NikolajBjorner added a commit that referenced this issue Jul 19, 2021

#5417

4388ab2

more gracefully handle non-implemented theories

NikolajBjorner added a commit that referenced this issue Jul 19, 2021

#5417 designate quantifier axioms as auxiliary

a648679

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

NikolajBjorner closed this as completed Jul 19, 2021

NikolajBjorner added a commit that referenced this issue Jul 19, 2021

#5417 again, refining root clauses above search level

49bd3ad

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Consolidated] issues with tactic.default_tactic=smt sat.euf=true #5417

[Consolidated] issues with tactic.default_tactic=smt sat.euf=true #5417

rainoftime commented Jul 18, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Jul 18, 2021 •

edited

Loading

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021 •

edited

Loading

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Jul 18, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

NikolajBjorner commented Jul 18, 2021

NikolajBjorner commented Jul 19, 2021

[Consolidated] issues with tactic.default_tactic=smt sat.euf=true #5417

[Consolidated] issues with tactic.default_tactic=smt sat.euf=true #5417

Comments

rainoftime commented Jul 18, 2021 • edited by NikolajBjorner Loading

rainoftime commented Jul 18, 2021 • edited Loading

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021 • edited Loading

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021 • edited by NikolajBjorner Loading

rainoftime commented Jul 18, 2021 • edited by NikolajBjorner Loading

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

rainoftime commented Jul 18, 2021

NikolajBjorner commented Jul 18, 2021

NikolajBjorner commented Jul 19, 2021

rainoftime commented Jul 18, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Jul 18, 2021 •

edited

Loading

rainoftime commented Jul 18, 2021 •

edited

Loading

rainoftime commented Jul 18, 2021 •

edited by NikolajBjorner

Loading

rainoftime commented Jul 18, 2021 •

edited by NikolajBjorner

Loading