reserved identifier violation #9

elfring · 2015-03-27T21:50:36Z

I would like to point out that identifiers like "_API_AST_MAP_H_" and "_SOLVER_H_" do eventually not fit to the expected naming convention of the C++ language standard.
Would you like to adjust your selection for unique names?

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

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

elfring · 2015-07-09T13:27:12Z

Are there any more update candidates left over?

nunoplopes · 2015-07-09T13:38:59Z

The fix was done on the unstable branch, not on master. I did a grep and there's nothing fundamental left behind.

elfring · 2015-07-09T13:45:28Z

How do think about to clean-up the use of double underscores in more identifiers?
Would you like to tamper with the reserved name space even less in your code base?

nunoplopes · 2015-07-09T13:57:48Z

Of course we aim to have fully well-defined code, which I'm sure we don't have at the moment.
Please feel to give concrete suggestions about what needs fixing. Thanks!

elfring · 2015-07-09T14:10:11Z

Examples for further update candidates:

DDNF__H_
SCOPED_PROOF__H_
Z3_PRIVATE__H_

fp unsat core extraction

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

Lev

Opt

…junctions After introducing the rewriter.sort_disjunctions option, I noticed a segfault in a Z3 run that was working fine for me. I traced the difference to a slight discrepancy between the first patch I submitted and the one we ended up merging: my first version would skip sorting the disjuncts in mk_nflat_core, but still return BR_DONE, while the patch in master returns BR_FAILED instead. This patch fixes the problem for me, and it makes slightly more sense to me to return a BR_DONE since, if `s` is true, some disjunct (e.g. a `false` or a repeat) might have been simplified away. However I don't fully understand this code. .. and I can't say I understand why the segfault happens. Perhaps that is a separate issue? This is the file to reproduce: https://gist.github.com/mtzguido/b7360c74d3d2e42d89f1bd9149ad26f6 Here's a stack trace of the failure, mk_nflat_or_core is not involved. ``` (gdb) where #0 0x0000555555b98497 in smt::context::get_lit_assignment(unsigned int) const () Z3Prover#1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const () Z3Prover#2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const () Z3Prover#3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const () Z3Prover#4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const () Z3Prover#5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) () Z3Prover#6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) () Z3Prover#7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) () Z3Prover#8 0x0000555555c9c1b7 in smt::context::decide() () Z3Prover#9 0x0000555555ca39fd in smt::context::bounded_search() () Z3Prover#10 0x0000555555ca30c2 in smt::context::search() () Z3Prover#11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) () Z3Prover#12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) () Z3Prover#13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) () Z3Prover#14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) () Z3Prover#15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) () Z3Prover#16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) () Z3Prover#17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) () Z3Prover#18 0x0000555556082ff0 in smt2::parser::parse_check_sat() () Z3Prover#19 0x0000555556084dc0 in smt2::parser::parse_cmd() () Z3Prover#20 0x00005555560861b6 in smt2::parser::operator()() () Z3Prover#21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) () Z3Prover#22 0x00005555555e8f68 in read_smtlib2_commands(char const*) () Z3Prover#23 0x00005555555ee6f6 in main () (gdb) ```

…junctions After introducing the rewriter.sort_disjunctions option (Z3Prover#6774), I noticed a segfault in a Z3 run that was working fine for me before the PR. I traced the difference to a slight discrepancy between the first patch I submitted and the one we ended up merging: my first version would skip sorting the disjuncts in mk_nflat_core, but still return BR_DONE, while the patch in master returns BR_FAILED instead. This patch fixes that problem, and it makes slightly more sense to me to return a BR_DONE since, if `s` is true, some disjunct (e.g. a `false` or a repeat) might have been simplified away. However I don't fully understand this code. ... and I can't say I understand why the segfault happens. Perhaps that is a separate issue? This is the file to reproduce: https://gist.github.com/mtzguido/b7360c74d3d2e42d89f1bd9149ad26f6 Here's a stack trace of the failure, mk_nflat_or_core is not involved. ``` (gdb) where #0 0x0000555555b98497 in smt::context::get_lit_assignment(unsigned int) const () Z3Prover#1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const () Z3Prover#2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const () Z3Prover#3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const () Z3Prover#4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const () Z3Prover#5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) () Z3Prover#6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) () Z3Prover#7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) () Z3Prover#8 0x0000555555c9c1b7 in smt::context::decide() () Z3Prover#9 0x0000555555ca39fd in smt::context::bounded_search() () Z3Prover#10 0x0000555555ca30c2 in smt::context::search() () Z3Prover#11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) () Z3Prover#12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) () Z3Prover#13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) () Z3Prover#14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) () Z3Prover#15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) () Z3Prover#16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) () Z3Prover#17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) () Z3Prover#18 0x0000555556082ff0 in smt2::parser::parse_check_sat() () Z3Prover#19 0x0000555556084dc0 in smt2::parser::parse_cmd() () Z3Prover#20 0x00005555560861b6 in smt2::parser::operator()() () Z3Prover#21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) () Z3Prover#22 0x00005555555e8f68 in read_smtlib2_commands(char const*) () Z3Prover#23 0x00005555555ee6f6 in main () (gdb) ```

…junctions (#6779) After introducing the rewriter.sort_disjunctions option (#6774), I noticed a segfault in a Z3 run that was working fine for me before the PR. I traced the difference to a slight discrepancy between the first patch I submitted and the one we ended up merging: my first version would skip sorting the disjuncts in mk_nflat_core, but still return BR_DONE, while the patch in master returns BR_FAILED instead. This patch fixes that problem, and it makes slightly more sense to me to return a BR_DONE since, if `s` is true, some disjunct (e.g. a `false` or a repeat) might have been simplified away. However I don't fully understand this code. ... and I can't say I understand why the segfault happens. Perhaps that is a separate issue? This is the file to reproduce: https://gist.github.com/mtzguido/b7360c74d3d2e42d89f1bd9149ad26f6 Here's a stack trace of the failure, mk_nflat_or_core is not involved. ``` (gdb) where #0 0x0000555555b98497 in smt::context::get_lit_assignment(unsigned int) const () #1 0x0000555555b984cb in smt::context::get_assignment(sat::literal) const () #2 0x0000555555b98504 in smt::context::get_assignment(unsigned int) const () #3 0x0000555555ca83b8 in smt::context::get_assignment_core(expr*) const () #4 0x0000555555c9af5a in smt::context::get_assignment(expr*) const () #5 0x0000555555d7bd1d in (anonymous namespace)::has_child_assigned_to(smt::context&, app*, lbool, expr*&, unsigned int) () #6 0x0000555555d7c413 in (anonymous namespace)::rel_case_split_queue::next_case_split_core(ptr_vector<expr>&, unsigned int&, unsigned int&, lbool&) () #7 0x0000555555d7c589 in (anonymous namespace)::rel_case_split_queue::next_case_split(unsigned int&, lbool&) () #8 0x0000555555c9c1b7 in smt::context::decide() () #9 0x0000555555ca39fd in smt::context::bounded_search() () #10 0x0000555555ca30c2 in smt::context::search() () #11 0x0000555555ca273d in smt::context::check(unsigned int, expr* const*, bool) () #12 0x0000555555cb166a in smt::kernel::check(unsigned int, expr* const*) () #13 0x0000555555cb9695 in (anonymous namespace)::smt_solver::check_sat_core2(unsigned int, expr* const*) () #14 0x00005555560dc0c6 in solver_na2as::check_sat_core(unsigned int, expr* const*) () #15 0x00005555560d73f3 in combined_solver::check_sat_core(unsigned int, expr* const*) () #16 0x00005555560d34e3 in solver::check_sat(unsigned int, expr* const*) () #17 0x0000555556097b26 in cmd_context::check_sat(unsigned int, expr* const*) () #18 0x0000555556082ff0 in smt2::parser::parse_check_sat() () #19 0x0000555556084dc0 in smt2::parser::parse_cmd() () #20 0x00005555560861b6 in smt2::parser::operator()() () #21 0x00005555560757e6 in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&, char const*) () #22 0x00005555555e8f68 in read_smtlib2_commands(char const*) () #23 0x00005555555ee6f6 in main () (gdb) ```

wintersteiger added the enhancement label May 23, 2015

itszor mentioned this issue Jun 1, 2015

Segfault with BitVector (lshr/extract), smt2 input #116

Closed

tautschnig mentioned this issue Jun 17, 2015

test/dl_context.cpp uses fixed (non-existent) path and segfaults #133

Closed

NikolajBjorner added a commit that referenced this issue Jul 9, 2015

update header guards to be C++ style. Fixes issue #9

4bc044c

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

NikolajBjorner closed this as completed Jul 9, 2015

wintersteiger referenced this issue in wintersteiger/z3 Aug 31, 2015

Merge pull request #9 from wintersteiger/smallFloats

c7981dc

fp unsat core extraction

agurfinkel pushed a commit to seahorn/z3 that referenced this issue Apr 2, 2016

update header guards to be C++ style. Fixes issue Z3Prover#9

b851d51

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

NikolajBjorner referenced this issue in NikolajBjorner/z3 May 23, 2016

Merge pull request #9 from NikolajBjorner/lev

b0a8365

Lev

NikolajBjorner mentioned this issue Sep 29, 2016

New packaging for and ability to distribute python bindings #735

Merged

qingkaishi mentioned this issue Nov 21, 2016

A double free issue #798

Closed

NikolajBjorner mentioned this issue Jul 1, 2017

Segmentation Fault in Java API #1125

Closed

This was referenced Jan 31, 2018

v4.5.0: ASSERTION VIOLATION File: ../src/util/vector.h Line: 243 #1468

Closed

v4.6.0: ASSERTION VIOLATION File: ../src/sat/sat_integrity_checker.cpp Line: 197 #1471

Closed

agurfinkel referenced this issue in agurfinkel/z3 May 14, 2018

Merge pull request #9 from TheRealNebus/opt

2d4d51d

Opt

levnach mentioned this issue Nov 28, 2018

Segmentation fault #1984

Closed

evmaus mentioned this issue May 24, 2019

Z3 and MSAN #2298

Closed

levnach mentioned this issue Mar 3, 2020

Debug branch: assertion violation at ../src/smt/theory_lra.cpp Line: 967 #3099

Closed

5hadowblad3 mentioned this issue Mar 16, 2020

use after free in ast.h 505 in both master and debug branch #3347

Closed

levnach mentioned this issue Mar 18, 2020

Debug and master branches: Assertion violation lp_primal_core_solver_def.h:1299 #3344

Closed

rainoftime mentioned this issue Apr 6, 2020

Segment fault at ast.h:504 (smt.core.minimize true + fp.xform.fix_unbound_vars ) #3817

Closed

rainoftime mentioned this issue Apr 24, 2020

heap-use-after-free on String formula at smt/theory_seq.h:171 (smt.threads 4, rewriter.sort_sums, rewriter.local_ctx, smt.arith.propagate_eqs false, rewriter.elim_and) #4085

Closed

rammohan02 mentioned this issue Feb 10, 2024

Segmentation fault while using python API solver.check() in linux #7117

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

reserved identifier violation #9

reserved identifier violation #9

elfring commented Mar 27, 2015

elfring commented Jul 9, 2015

nunoplopes commented Jul 9, 2015

elfring commented Jul 9, 2015

nunoplopes commented Jul 9, 2015

elfring commented Jul 9, 2015

reserved identifier violation #9

reserved identifier violation #9

Comments

elfring commented Mar 27, 2015

elfring commented Jul 9, 2015

nunoplopes commented Jul 9, 2015

elfring commented Jul 9, 2015

nunoplopes commented Jul 9, 2015

elfring commented Jul 9, 2015