Databases
StackOverflow2013
Postsdbo
POIZ3 cpp_example segmentation fault
Body
 

Note that there are some explanatory texts on larger screens.

plurals
  1. POIZ3 cpp_example segmentation fault
    text
    copied!<p>I get a segfault when using the latest version of IZ3 and running the cpp_example.</p> <p>To reproduce:</p> <ul> <li>Clone z3: <code>git clone https://git01.codeplex.com/z3</code></li> <li>Switch to branch <code>interp</code>: <code>git checkout interp</code></li> <li>Build following the build instructions in <code>README</code></li> <li>Additionally, build <code>cpp_example</code>: <code>cd build ; make cpp_example</code></li> <li>Run the <code>cpp_example</code></li> <li><p>Result:</p> <pre><code>unsat core example 3 [1] 30687 segmentation fault ./cpp_example </code></pre></li> </ul> <p>The <code>cpp_example</code> works for me if I build on <code>master</code>.</p> <p>I read a message on some mailing list dating from December 2012 that the interpolating version of Z3 could not be built against the latest version of Z3, but that this was a work in progress.</p> <p>Does IZ3 still not work with Z3 version 4?</p> <p>If yes, are there any instructions on how to build the interpolating sources against an earlier version of Z3? (Starting with: where to obtain the source code of IZ3-3.2 or whatever?)</p> <ul> <li>Edit:</li> <li>OS: <code>Linux __ 2.6.37.6-24-desktop #1 SMP PREEMPT __ i686 i686 i386 GNU/Linux</code></li> <li><p>g++:</p> <pre><code>Using built-in specs. COLLECT_GCC=g++ COLLECT_LTO_WRAPPER=/usr/lib/gcc/i586-suse-linux/4.5/lto-wrapper Target: i586-suse-linux Configured with: ../configure --prefix=/usr --infodir=/usr/share/info --mandir=/usr/share/man --libdir=/usr/lib --libexecdir=/usr/lib --enable-languages=c,c++,objc,fortran,obj-c++,java,ada --enable-checking=release --with-gxx-include-dir=/usr/include/c++/4.5 --enable-ssp --disable-libssp --disable-plugin --with-bugurl=http://bugs.opensuse.org/ --with-pkgversion='SUSE Linux' --disable-libgcj --disable-libmudflap --with-slibdir=/lib --with-system-zlib --enable-__cxa_atexit --enable-libstdcxx-allocator=new --disable-libstdcxx-pch --enable-version-specific-runtime-libs --program-suffix=-4.5 --enable-linux-futex --without-system-libunwind --enable-gold --with-plugin-ld=/usr/bin/gold --with-arch-32=i586 --with-tune=generic --build=i586-suse-linux Thread model: posix </code></pre></li> </ul>
 

Querying!

 
Guidance
An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload