1

Closed

segmentation fault on get-unsat-core

description

Hi,
I get a segmentation fault with the attached SMTLIB 2 file. See the gdb backtrace below. Without the get-unsat-core, z3 runs fine. This is using the 4.3.1 Master branch release, compiled on a x86_64 Linux platform (Scientific Linux 6.3). z3 4.0 runs fine on this example.

-Paul.
Program received signal SIGSEGV, Segmentation fault.                            
0x0000000000ba1624 in ast_manager::linearize(dependency_manager<ast_manager::ex\
pr_dependency_config>::dependency*, ptr_vector<expr>&) ()                       
Missing separate debuginfos, use: debuginfo-install glibc-2.12-1.80.el6_3.5.x86\
_64 libgcc-4.4.6-4.el6.x86_64 libgomp-4.4.6-4.el6.x86_64 libstdc++-4.4.6-4.el6.\
x86_64                                                                          
(gdb) bt                                                                        
#0  0x0000000000ba1624 in ast_manager::linearize(dependency_manager<ast_manager\
::expr_dependency_config>::dependency*, ptr_vector<expr>&) ()                   
#1  0x000000000094cfcb in get_unsat_core_cmd::execute(cmd_context&) ()          
#2  0x0000000000942c65 in smt2::parser::parse_cmd() ()                          
#3  0x0000000000943748 in smt2::parser::operator()() ()                         
#4  0x000000000093332a in parse_smt2_commands(cmd_context&, std::basic_istream<\
char, std::char_traits<char> >&, bool) ()                                       
#5  0x000000000043694d in read_smtlib2_commands(char const*, front_end_params&)\
 ()                                                                             
#6  0x00000000004356cd in main ()

file attachments

Closed Feb 19 at 6:11 PM by leodemoura
This bug has been fixed.

comments

leodemoura wrote Feb 19 at 6:11 PM

Hi Paul,

This bug has been fixed in the unstable (work-in-progress) branch. The fix will be available in the next release.
In the meantime, you can avoid the bug by compiling the unstable branch, or downloading one of the nightly builds.

Thanks,
Leo

PaulJackson wrote Feb 21 at 11:53 AM

Hi Leo,

I grabbed the nightly build z3-4.3.2.18bae817316b-x64-debian-6.0.6. The z3 binary included there seems to run OK on the Scientific Linux 6.3 I use. 56 instances I see of the reported error go away, but I still get one segmentation fault with a virtually identical backtrace (see below). The .smt2 file causing this segfault is attached.

Paul.
Program received signal SIGSEGV, Segmentation fault.
0x0000000000c3a004 in ast_manager::linearize(dependency_manager<ast_manager::expr_dependency_config>::dependency*, ptr_vector<expr>&) ()
Missing separate debuginfos, use: debuginfo-install glibc-2.12-1.80.el6_3.5.x86_64 libgcc-4.4.6-3.el6.x86_64 libgomp-4.4.6-3.el6.x86_64 libstdc++-4.4.6-3.el6.x86_64
(gdb) bt
#0  0x0000000000c3a004 in ast_manager::linearize(dependency_manager<ast_manager::expr_dependency_config>::dependency*, ptr_vector<expr>&) ()
#1  0x00000000009ef4ee in tactic2solver::check_sat_core(unsigned int, expr* const*) ()
#2  0x00000000009f0ee1 in solver_na2as::check_sat(unsigned int, expr* const*) ()
#3  0x00000000009f2933 in combined_solver::check_sat(unsigned int, expr* const*) ()
#4  0x00000000009ded4a in cmd_context::check_sat(unsigned int, expr* const*) ()
#5  0x00000000009a9bbb in smt2::parser::parse_check_sat() ()
#6  0x00000000009b2600 in smt2::parser::parse_cmd() ()
#7  0x00000000009b2b18 in smt2::parser::operator()() ()
#8  0x00000000009a21ed in parse_smt2_commands(cmd_context&, std::basic_istream<char, std::char_traits<char> >&, bool, params_ref const&) ()
#9  0x00000000004390d9 in read_smtlib2_commands(char const*) ()
#10 0x000000000043a0da in main ()

leodemoura wrote Feb 21 at 6:04 PM

Hi Paul,

Thanks for sending the new problem. I fixed the bug exposed by the new problem.
The fix is already available in the unstable branch.
http://z3.codeplex.com/SourceControl/changeset/4922d62311c3

Cheers,
Leo

Sign in to add a comment