Reporting zero-valued statistics

Hi, I am processing the output of Z3 with regexs for various scripts I use to conduct experiments. I ran into a bug in my scripts today when certain inputs cause Z3 to finish "in zero time". A...

Id #105 | Release: None | Updated: Apr 8 at 1:18 PM by switicus | Created: Apr 8 at 11:30 AM by switicus

Unstable branch releases broken?

Hi there.. I'm trying to follow the unstable-branch on OS-X closely. It appears that the last 15 nightly builds are all called the same: z3-4.3.2.d548c51a984e-x64-osx-10.8.5.zip I thought the h...

Id #91 | Release: None | Updated: Feb 15 at 4:32 PM by LeventErkok | Created: Feb 15 at 4:32 PM by LeventErkok

AUFNIRA SMT-LIB compliance bug

The following two line SMT-LIB seems to be correct according to the AUFNIRA definition. http://smtlib.cs.uiowa.edu/logics/AUFNIRA.smt2 since (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_r...

Id #90 | Release: None | Updated: Mar 24 at 10:46 PM by Heizmann | Created: Feb 13 at 5:54 PM by Heizmann

patch/review: QF_GABV logic

Hello, We sometimes use a logic comprised of QF_ABV plus the "as const" array construct. I recently did an experiment where I extended z3 with a QF_GABV logic (GA = Generalized Arrays). I added...

Id #78 | Release: None | Updated: Mar 20 at 4:02 AM by NBjorner | Created: Nov 26, 2013 at 8:10 PM by dvitek

libc++abi.dylib: terminate called throwing an exception

In our work with MetiTarski and z3, we use the :timeout option for calls of (check-sat-using). Many repeated calls to z3 (4.3.1) are taking place. With OSX 10.8.5 and XCode 5, if you repeatedly cal...

Id #70 | Release: None | Updated: Oct 15, 2013 at 2:25 PM by ic3guy | Created: Oct 15, 2013 at 10:21 AM by ic3guy

deadlock in free on timeout on win64

I think we're basically seeing the windows version of issue 21 here. If the timeout timer goes off while the main thread is holding a heap lock (perhaps because it is executing malloc or free), th...

Id #42 | Release: None | Updated: Jun 2, 2013 at 6:47 PM by NikolajBjorner | Created: May 29, 2013 at 5:53 PM by dvitek

timeout signal handler invokes non-signal-safe functions

On platforms where z3 uses signals to implement timeouts (anything but mac/windows), z3 has a race where it can run into problems when it invokes non-async-signal-safe functions from inside the tim...

Id #21 | Release: None | Updated: Feb 7, 2013 at 7:19 PM by dvitek | Created: Feb 6, 2013 at 5:35 PM by dvitek

(check-sat) of 4-queens problem returns unknown

When I submit the attached file with a SMT-problem description for the n-queens problem with n=4 to Z3 4.1.2 (downloaded yesterday, the z3 /version reports V4.2, though), I get an unknown upon the ...

Id #2 | Release: None | Updated: Jan 24 at 10:52 PM by rybal | Created: Oct 9, 2012 at 9:44 AM by Adorf

  • 1-8 of 8 Work Items
    • Previous
    • 1
    • Next
    • Showing
    • All
    • Work Items