Issues on arithmetic, string, and datatype formulas #5323

rainoftime · 2021-06-01T00:52:15Z

Hi, for the following formula,
z3 e2c5e2e

(set-option :smt.random_seed 9)
(assert (exists ((x Real)) (= (* x x) 2.0)))
(push)
(check-sat)
(check-sat-using qfnia)

id: 271
Leaked: RootObject[@10]
id: 272
=================================================================
==77325==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 24 byte(s) in 1 object(s) allocated from:
    #0 0x50b2e8 in __interceptor_malloc /home//llvm-6/compiler-rt/lib/asan/asan_malloc_linux.cc:88
    #1 0x414faa0 in memory::allocate(unsigned long) /home/z3/build/../src/util/memory_manager.cpp:273:16
    #2 0x414f8bf in memory::allocate(char const*, int, char const*, unsigned long) /home/z3/build/../src/util/memory_manager.cpp:212:16
    #3 0x14fcd73 in smt::theory_lra::imp::mk_value(smt::enode*, smt::model_generator&) /home/z3/build/../src/smt/theory_lra.cpp:3278:20
    #4 0x14f3e20 in smt::theory_lra::mk_value(smt::enode*, smt::model_generator&) /home/z3/build/../src/smt/theory_lra.cpp:3838:19
    #5 0x193ba25 in smt::model_generator::mk_value_procs(obj_map<smt::enode, smt::model_value_proc*>&, ptr_vector<smt::enode>&, ptr_vector<smt::model_value_proc>&) /home/z3/build/../src/smt/smt_model_generator.cpp:115:40
    #6 0x193fd47 in smt::model_generator::mk_values() /home/z3/build/../src/smt/smt_model_generator.cpp:300:9
    #7 0x1945203 in smt::model_generator::mk_model() /home/z3/build/../src/smt/smt_model_generator.cpp:502:9
    #8 0x1c147b8 in smt::context::mk_proto_model() /home/z3/build/../src/smt/smt_context.cpp:4515:48
    #9 0x1c0c901 in smt::context::get_model(ref<model>&) /home/z3/build/../src/smt/smt_context.cpp:4550:13
    #10 0x1b2b9bc in smt::kernel::imp::get_model(ref<model>&) /home/z3/build/../src/smt/smt_kernel.cpp:136:22
    #11 0x1b2a484 in smt::kernel::get_model(ref<model>&) /home/z3/build/../src/smt/smt_kernel.cpp:352:16
    #12 0x1290561 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/smt/tactic/smt_tactic_core.cpp:224:28
    #13 0x2d2f3c3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:119:19
    #14 0x2d421d7 in try_for_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:948:18
    #15 0x2d313bf in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:291:24
    #16 0x2d2f3c3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:119:19
    #17 0x2d2f3c3 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:119:19
    #18 0x2d4057c in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactical.cpp:775:14
    #19 0x2d824e6 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /home/z3/build/../src/tactic/tactic.cpp:150:9
    #20 0x2d82d94 in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) /home/z3/build/../src/tactic/tactic.cpp:170:9
    #21 0x2bf4115 in check_sat_using_tactict_cmd::execute(cmd_context&) /home/z3/build/../src/cmd_context/tactic_cmds.cpp:216:25
    #22 0x2b771e7 in smt2::parser::parse_ext_cmd(int, int) /home/z3/build/../src/parsers/smt2/smt2parser.cpp:2906:33
    #23 0x2b6ef68 in smt2::parser::parse_cmd() /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3012:13
    #24 0x2b6959c in smt2::parser::operator()() /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3141:29
    #25 0x2b67e88 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /home/z3/build/../src/parsers/smt2/smt2parser.cpp:3190:12
    #26 0x55b275 in read_smtlib2_commands(char const*) /home/z3/build/../src/shell/smtlib_frontend.cpp:142:18
    #27 0x547a19 in main /home/z3/build/../src/shell/main.cpp:371:28
    #28 0x7f56903f883f in __libc_start_main /build/glibc-e6zv40/glibc-2.23/csu/../csu/libc-start.c:291

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

rainoftime · 2021-06-01T03:37:01Z

(rewriter.expand_nested_stores) Assertion error src/smt/tactic/ctx_solver_simplify_tactic.cpp:138

(set-option :rewriter.expand_nested_stores true)
(declare-fun v6 () (_ BitVec 32))
(assert (forall ((v7 (_ BitVec 32))) (exists ((a1 (Array (_ BitVec 32) (_ BitVec 8)))) (not (= (_ bv0 1) (bvor (bvcomp (_ bv0 2) ((_ extract 1 0) v7)) (bvashr (bvnot (ite (= (store (store (store (store a1 v7 ((_ extract 15 8) v7)) (_ bv1 32) ((_ extract 7 0) v6)) (bvadd v6 (_ bv1 32)) ((_ extract 15 8) v6)) v6 ((_ extract 31 24) v6)) (store (store (store (store a1 (_ bv1 32) ((_ extract 7 0) v6)) (bvadd v6 (_ bv1 32)) ((_ extract 15 8) v6)) v6 ((_ extract 31 24) v6)) v7 ((_ extract 31 24) v7))) (_ bv1 1) (_ bv0 1))) (bvcomp (_ bv0 2) ((_ extract 1 0) v6)))))))))
(check-sat-using (then purify-arith ctx-solver-simplify))

z3 delta.out.smt2 
ASSERTION VIOLATION
File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp
Line: 138
UNEXPECTED CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

rainoftime · 2021-06-01T03:46:07Z

(default) heap-use-after-free at ast.h:502

(declare-fun c () (Seq (Seq Int)))
(declare-fun b () (Seq (Seq Int)))
(assert (forall ((d (Seq (Seq Int)))) (forall ((f (Seq Int))) (exists ((a (Seq (Seq Int)))) (exists ((e (Seq Int))) (and (= a (seq.++ (seq.unit e) b)) (distinct (seq.++ (seq.unit f) d) a c)))))))
(check-sat)

==139830==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070001b9e34 at pc 0x0000005bcd67 bp 0x7ffd0a136470 sp 0x7ffd0a136468
READ of size 4 at 0x6070001b9e34 thread T0
    #0 0x5bcd66 in ast::hash() const /z3/build/../src/ast/ast.h:502:36
    #1 0x8988b3 in obj_ptr_pair_hash<expr, expr>::operator()(std::pair<expr*, expr*> const&) const /z3/build/../src/util/hash.h:176:38
    #2 0x8986ff in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::get_hash(std::pair<expr*, expr*> const&) const /hom
e/z3-debug/build/../src/util/hashtable.h:152:64
    #3 0x202a6c6 in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::remove(std::pair<expr*, expr*> const&) /z3-debug/build/../src/util/hashtable.h:558:25
    #4 0x200bdbc in core_hashtable<obj_pair_hash_entry<expr, expr>, obj_ptr_pair_hash<expr, expr>, default_eq<std::pair<expr*, expr*> > >::erase(std::pair<expr*, expr*> const&) /z3-debug/build/../src/util/hashtable.h:591:34
    #5 0x2106427 in remove_obj_pair_map::undo() /z3/build/../src/smt/seq_eq_solver.cpp:1124:15
    #6 0xfaea1f in undo_trail_stack(ptr_vector<trail>&, unsigned int) /z3/build/../src/util/trail.h:388:16
    #7 0x18167e3 in smt::context::undo_trail_stack(unsigned int) /z3/build/../src/smt/smt_context.cpp:1944:9
    #8 0x181d90a in smt::context::pop_scope_core(unsigned int) /z3/build/../src/smt/smt_context.cpp:2429:13
    #9 0x183892b in smt::context::resolve_conflict() /z3/build/../src/smt/smt_context.cpp:4091:38
    #10 0x183103c in smt::context::bounded_search() /z3/build/../src/smt/smt_context.cpp:3799:22
    #11 0x182e0ab in smt::context::search() /z3/build/../src/smt/smt_context.cpp:3678:22
    #12 0x182d2a4 in smt::context::check(unsigned int, expr* const*, bool) /z3/build/../src/smt/smt_context.cpp:3561:17
    #13 0x182c6c2 in smt::context::setup_and_check(bool) /z3/build/../src/smt/smt_context.cpp:3497:20
    #14 0x13d54a9 in smt::kernel::imp::setup_and_check() /z3/build/../src/smt/smt_kernel.cpp:108:29
    #15 0x13d3d6c in smt::kernel::setup_and_check() /z3/build/../src/smt/smt_kernel.cpp:326:23
    #16 0x126de94 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /z3/build/../src/smt/tactic/smt_tactic_core.cpp:201:32
    #17 0x2cf44bf in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /z3/build/../src/tactic/tactical.cpp:119:19
    #18 0x2d08943 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /z3/build/../src/tactic/tactical.cpp:1038:19
    #19 0x2d08943 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /z3/build/../src/tactic/tactical.cpp:1038:19

rainoftime · 2021-06-04T14:35:39Z

z3 7c86134

(declare-fun f (Bool) Bool)
(assert (forall ((v8 Bool)) (forall ((v7 Bool)) (f (= v7 v8)))))
(check-sat-using (then simplify reduce-invertible ufbv-rewriter))

z3-debug/build/z3 delta.out.smt2
ASSERTION VIOLATION
File: ../src/ast/macros/macro_util.cpp
Line: 472
is_macro_head(head, head->get_num_args()) || is_quasi_macro_ok(head, head->get_num_args(), def)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

rainoftime · 2021-06-05T07:06:33Z

rewriter.eq2ineq + model_validate

(set-option :rewriter.eq2ineq true)
(assert (exists ((x Int)) (not (and (= x (bv2int ((_ int2bv 1) x))) (not (= x (bv2int ((_ int2bv 1) x))))))))
(push)
(check-sat)
(check-sat-using qffd)

sat
failed to verify: (exists ((x Int))
  (let ((a!1 (and (<= x (bv2int ((_ int2bv 1) x)))
                  (>= x (bv2int ((_ int2bv 1) x))))))
  (let ((a!2 (and (<= x (bv2int ((_ int2bv 1) x)))
                  (>= x (bv2int ((_ int2bv 1) x)))
                  (not a!1))))
    (not a!2))))
evaluated to (exists ((x Int))
  (let ((a!1 (and (<= x (bv2int ((_ int2bv 1) x)))
                  (>= x (bv2int ((_ int2bv 1) x))))))
  (let ((a!2 (and (<= x (bv2int ((_ int2bv 1) x)))
                  (>= x (bv2int ((_ int2bv 1) x)))
                  (not a!1))))
    (not a!2))))
(params keep_cardinality_constraints true pb.solver solver)

=================================================================
==49110==ERROR: LeakSanitizer: detected memory leaks

rainoftime · 2021-06-08T03:19:44Z

(declare-datatypes ((A 0) (B 0)) (((a (sa B))) ((e1) (e2 (se2 A)))))
(assert (forall ((x1 A)) (exists ((x2 B)) (let (($x23 (= x1 (a x2))))))))
(check-sat-using qfufbv_ackr)

AddressSanitizer:DEADLYSIGNAL
=================================================================
==73595==ERROR: AddressSanitizer: stack-overflow on address 0x7fffe21e8ba8 (pc 0x0000004a5d17 
bp 0x7fffe21e9420 sp 0x7fffe21e8bb0 T0)
    #0 0x4a5d16 in __interceptor_strlen.part.32 /home/heqing/llvm-6/compiler-rt/lib/asan/../sa
nitizer_common/sanitizer_common_interceptors.inc:332
    #1 0x8f015b in str_hash_proc::operator()(char const*) const /home/peisen/test/tofuzz/z3-de
bug/build/../src/util/str_hashtable.h:27:93
    #2 0x40cff2c in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::ge
t_hash(char const* const&) const /z3/build/../src/util/hashtable
.h:152:64
    #3 0x40d0df1 in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::fi
nd_core(char const* const&) const /z3/build/../src/util/hashtabl
e.h:506:25
    #4 0x40cf02c in core_hashtable<ptr_hash_entry<char const>, str_hash_proc, str_eq_proc>::co
ntains(char const* const&) const /z3/build/../src/util/hashtable
.h:531:16
    #5 0x415f790 in is_debug_enabled(char const*) /z3/build/../s
rc/util/debug.cpp:75:34
    #6 0x3be448b in ast_manager::register_node_core(ast*) /z3/bu
ild/../src/ast/ast.cpp:1727:5
    #7 0x3c08b6c in app* ast_manager::register_node<app>(app*) /z3-deb
ug/build/../src/ast/ast.h:1659:33

    #12 0x2e2954e in datatype_factory::get_fresh_value(sort*) /h

rainoftime · 2021-06-20T07:41:02Z

z3 2138ef2
heap-use-after-free at src/qe/mbp/mbp_arith.cpp:286:28

(declare-fun i5 () Int)
(declare-fun v41 () Bool)
(assert (distinct (forall ((q312 Bool) (q313 Int)) (or (not (= v41 q312)) (= q313 (abs (abs i5)))))))
(check-sat-using qe_rec)

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

rainoftime · 2021-06-23T04:00:50Z

heap-use-after-free at ./src/util/obj_hashtable.h:87:46
z3 d5c6abe

(declare-const x Bool)
(declare-datatypes ((ms 0)) (((e) (i) (t))))
(declare-sort d)
(declare-datatypes ((m 0)) (((c_ (m ms) (m_ d)))))
(declare-datatypes ((B 0)) (((T) (F))))
(declare-sort n)
(declare-fun r () n)
(declare-fun h () (Array n m))
(declare-fun s () (Array n B))
(assert (forall ((c (Array n m))) (and (distinct t (m (c r))) (= i (m (c r))) (forall ((n n)) (= i (m (c n)))) (= h (store c r (c_ e (m_ (select h r))))) (forall ((n n)) (or x (= (select s r) (ite (distinct n r) T F)))))))
(check-sat-using (then nnf unit-subsume-simplify ufbv))

rainoftime · 2021-06-23T04:01:47Z

Assertion error at src/util/obj_hashtable.h:174

(set-option :smt.phase_selection 5)
(declare-sort S)
(declare-datatypes ((lst 1)) ((par (k!00) ((nil) (cons (car k!00) (cdr (lst k!00)))))))
(declare-fun l1 () (lst S))
(assert (exists ((l2 (lst S))) (not (= l1 l2))))
(check-sat-using ctx-solver-simplify)

z3 delta.out.smt2 
ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 174
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

#5323 (comment)

NikolajBjorner · 2021-07-18T12:17:34Z

qffd with non fd input (int2bv/bv2int) will not be fixed as it is outside qffd use. Other bugs that could be addressed have been

@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>

rainoftime changed the title ~~Issues on arithmetic formulas~~ Issues on arithmetic and string formulas Jun 1, 2021

NikolajBjorner added a commit that referenced this issue Jun 20, 2021

#5323 heap use after free

45228bf

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

rainoftime changed the title ~~Issues on arithmetic and string formulas~~ Issues on arithmetic, string, and datatype formulas Jun 23, 2021

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

#5323

cde3eac

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

#5323

284d599

#5323 (comment)

NikolajBjorner closed this as completed Jul 18, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Issues on arithmetic, string, and datatype formulas #5323

Issues on arithmetic, string, and datatype formulas #5323

rainoftime commented Jun 1, 2021 •

edited

Loading

rainoftime commented Jun 1, 2021 •

edited

Loading

rainoftime commented Jun 1, 2021 •

edited

Loading

rainoftime commented Jun 4, 2021 •

edited

Loading

rainoftime commented Jun 5, 2021

rainoftime commented Jun 8, 2021

rainoftime commented Jun 20, 2021 •

edited

Loading

rainoftime commented Jun 23, 2021

rainoftime commented Jun 23, 2021

NikolajBjorner commented Jul 18, 2021

Issues on arithmetic, string, and datatype formulas #5323

Issues on arithmetic, string, and datatype formulas #5323

Comments

rainoftime commented Jun 1, 2021 • edited Loading

rainoftime commented Jun 1, 2021 • edited Loading

rainoftime commented Jun 1, 2021 • edited Loading

rainoftime commented Jun 4, 2021 • edited Loading

rainoftime commented Jun 5, 2021

rainoftime commented Jun 8, 2021

rainoftime commented Jun 20, 2021 • edited Loading

rainoftime commented Jun 23, 2021

rainoftime commented Jun 23, 2021

NikolajBjorner commented Jul 18, 2021

rainoftime commented Jun 1, 2021 •

edited

Loading

rainoftime commented Jun 1, 2021 •

edited

Loading

rainoftime commented Jun 1, 2021 •

edited

Loading

rainoftime commented Jun 4, 2021 •

edited

Loading

rainoftime commented Jun 20, 2021 •

edited

Loading