[macOS] Build uses unsupported flags which break it: `cc1plus: error: '-fno-fat-lto-objects' are supported only with linker plugin`
barracuda156 opened this issue · 40 comments
barracuda156 commented
---> Building vampire
Executing: cd "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build" && ninja -j6 all -j6 -v
[1/243] /opt/local/bin/g++-mp-13 -DCHECK_LEAKS=0 -DVDEBUG=0 -DVTIME_PROFILING=0 -DVZ3=1 -I/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375 -isystem /opt/local/include -pipe -mcpu=native -mtune=native -DNDEBUG -I/opt/local/include -D_GLIBCXX_USE_CXX11_ABI=0 -O3 -DNDEBUG -flto=auto -fno-fat-lto-objects -arch ppc -mmacosx-version-min=10.6 -Wall -fno-threadsafe-statics -fno-rtti -fsized-deallocation -std=c++14 -MD -MT CMakeFiles/obj.dir/Debug/Tracer.cpp.o -MF CMakeFiles/obj.dir/Debug/Tracer.cpp.o.d -o CMakeFiles/obj.dir/Debug/Tracer.cpp.o -c /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Debug/Tracer.cpp
FAILED: CMakeFiles/obj.dir/Debug/Tracer.cpp.o
/opt/local/bin/g++-mp-13 -DCHECK_LEAKS=0 -DVDEBUG=0 -DVTIME_PROFILING=0 -DVZ3=1 -I/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375 -isystem /opt/local/include -pipe -mcpu=native -mtune=native -DNDEBUG -I/opt/local/include -D_GLIBCXX_USE_CXX11_ABI=0 -O3 -DNDEBUG -flto=auto -fno-fat-lto-objects -arch ppc -mmacosx-version-min=10.6 -Wall -fno-threadsafe-statics -fno-rtti -fsized-deallocation -std=c++14 -MD -MT CMakeFiles/obj.dir/Debug/Tracer.cpp.o -MF CMakeFiles/obj.dir/Debug/Tracer.cpp.o.d -o CMakeFiles/obj.dir/Debug/Tracer.cpp.o -c /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Debug/Tracer.cpp
cc1plus: error: '-fno-fat-lto-objects' are supported only with linker plugin
[2/243] /opt/local/bin/g++-mp-13 -DCHECK_LEAKS=0 -DVDEBUG=0 -DVTIME_PROFILING=0 -DVZ3=1 -I/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375 -isystem /opt/local/include -pipe -mcpu=native -mtune=native -DNDEBUG -I/opt/local/include -D_GLIBCXX_USE_CXX11_ABI=0 -O3 -DNDEBUG -flto=auto -fno-fat-lto-objects -arch ppc -mmacosx-version-min=10.6 -Wall -fno-threadsafe-statics -fno-rtti -fsized-deallocation -std=c++14 -MD -MT CMakeFiles/obj.dir/Debug/Assertion.cpp.o -MF CMakeFiles/obj.dir/Debug/Assertion.cpp.o.d -o CMakeFiles/obj.dir/Debug/Assertion.cpp.o -c /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Debug/Assertion.cpp
FAILED: CMakeFiles/obj.dir/Debug/Assertion.cpp.o
/opt/local/bin/g++-mp-13 -DCHECK_LEAKS=0 -DVDEBUG=0 -DVTIME_PROFILING=0 -DVZ3=1 -I/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375 -isystem /opt/local/include -pipe -mcpu=native -mtune=native -DNDEBUG -I/opt/local/include -D_GLIBCXX_USE_CXX11_ABI=0 -O3 -DNDEBUG -flto=auto -fno-fat-lto-objects -arch ppc -mmacosx-version-min=10.6 -Wall -fno-threadsafe-statics -fno-rtti -fsized-deallocation -std=c++14 -MD -MT CMakeFiles/obj.dir/Debug/Assertion.cpp.o -MF CMakeFiles/obj.dir/Debug/Assertion.cpp.o.d -o CMakeFiles/obj.dir/Debug/Assertion.cpp.o -c /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Debug/Assertion.cpp
cc1plus: error: '-fno-fat-lto-objects' are supported only with linker plugin
MichaelRawson commented
Hi @barracuda156 - thanks for the report. Could you say how you configured the build? LTO/IPO should not be enabled by default.
Also - I think this is for PowerPC, right? Let us know how you get on, we'd be interested to know if Vampire works.
barracuda156 commented
Apparently the issue is that ld does not support LTO on older macOS, however I am not sure where the flag itself comes from. GCC itself supports it: https://gcc.gnu.org/onlinedocs/gcc/Optimize-Options.html (however notice comments there).
Test for LTO in fact fails, but why does the build proceeds with LTO enabled? It should just disable it instead.
This is apparently a configure test error:
CXX compiler IPO check failed with the following output:
Change Dir: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/CMakeFiles/_CMakeLTOTest-CXX/bin
Run Build Command(s):ninja && [1/4] Building CXX object CMakeFiles/foo.dir/foo.cpp.o
FAILED: CMakeFiles/foo.dir/foo.cpp.o
/opt/local/bin/g++-mp-13 -pipe -mcpu=native -mtune=native -DNDEBUG -I/opt/local/include -D_GLIBCXX_USE_CXX11_ABI=0 -flto=auto -fno-fat-lto-objects -isysroot /Developer/SDKs/MacOSX10.6.sdk -mmacosx-version-min=10.6 -o CMakeFiles/foo.dir/foo.cpp.o -c /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/CMakeFiles/_CMakeLTOTest-CXX/src/foo.cpp
cc1plus: error: '-fno-fat-lto-objects' are supported only with linker plugin
[2/4] Building CXX object CMakeFiles/boo.dir/main.cpp.o
FAILED: CMakeFiles/boo.dir/main.cpp.o
/opt/local/bin/g++-mp-13 -pipe -mcpu=native -mtune=native -DNDEBUG -I/opt/local/include -D_GLIBCXX_USE_CXX11_ABI=0 -flto=auto -fno-fat-lto-objects -isysroot /Developer/SDKs/MacOSX10.6.sdk -mmacosx-version-min=10.6 -o CMakeFiles/boo.dir/main.cpp.o -c /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/CMakeFiles/_CMakeLTOTest-CXX/src/main.cpp
cc1plus: error: '-fno-fat-lto-objects' are supported only with linker plugin
ninja: build stopped: subcommand failed.
barracuda156 commented
@MichaelRawson Thank you for responding!
I guess it is Macports portfile forces this option: https://github.com/macports/macports-ports/blob/c7df747729c62f2801614020663ef140a33663e1/math/vampire/Portfile#L33
configure.args -DIPO=ON
I wanted to update the port, which is at some archaic version at the moment, left this configure arg as it was there.
I can disable it and retry the build. (I could also explicitly disable LTO by passing relevant cxx flags to gcc.)
I think this is for PowerPC, right? Let us know how you get on, we'd be interested to know if Vampire works.
Yes. Once the build itself works, I will run tests and let you know.
barracuda156 commented
@MichaelRawson Disabling IPO worked, but then the build fails here:
/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Lib/Portability.hpp:23:20: error: static assertion failed: Vampire assumes that the size of a pointer is 8 bytes for efficiency reasons. This may be fixed/relaxed in future, but for the moment expect problems if running on other architectures.
23 | sizeof(void *) == 8,
| ~~~~~~~~~~~~~~~^~~~
/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Lib/Portability.hpp:23:20: note: the comparison reduces to '(4 == 8)'
barracuda156 commented
And then:
In file included from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Debug/TimeProfiling.hpp:19,
from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Lib/Metaiterators.hpp:29,
from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Lib/Set.hpp:26,
from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Indexing/TermSharing.hpp:20,
from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Lib/Environment.cpp:20:
/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Kernel/Term.hpp:260:20: error: static assertion failed: size of TermList must be the same size as that of size_t
260 | sizeof(TermList) == sizeof(size_t),
| ~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~
/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-31939a4a3bf99dd8329faf947b8a1f2088eea375/Kernel/Term.hpp:260:20: note: the comparison reduces to '(8 == 4)'
barracuda156 commented
I have disabled static_asserts, build succeeds, tests are blocked by sandboxing, it seems:
---> Testing vampire
Executing: cd "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build" && ninja test
[0/1] Running tests...
Test project /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
Start 1: DHMap
sh: /bin/ps: Operation not permitted
1/34 Test #1: DHMap .............................***Timeout 101.58 sec
Start 2: QuotientE
sh: /bin/ps: Operation not permitted
2/34 Test #2: QuotientE .........................***Timeout 99.41 sec
Start 3: UnificationWithAbstraction
sh: /bin/ps: Operation not permitted
3/34 Test #3: UnificationWithAbstraction ........***Timeout 96.88 sec
I may know a fix, will rerun the build.
barracuda156 commented
@MichaelRawson So no, it is broken, as of now. Sandboxing error is trivially fixable, but the binary is broken anyway:
(gdb) run
Starting program: /opt/local/bin/vampire
Reading symbols for shared libraries +++++.... done
Program received signal EXC_BAD_ACCESS, Could not access memory.
Reason: KERN_PROTECTION_FAILURE at address: 0x0000000a
0x0002e930 in Kernel::Term::functor ()
barracuda156 commented
(gdb) where
#0 0x0002e930 in Kernel::Term::functor ()
#1 0x00039b6c in Kernel::Term::isSpecial ()
#2 0x0005a604 in Kernel::Term::toString ()
#3 0x0005a540 in Kernel::TermList::toString ()
#4 0x00054a74 in Kernel::OperatorType::toString ()
#5 0x0004a51c in Kernel::Signature::addInterpretedPredicate ()
#6 0x0004a1d4 in Kernel::Signature::addEquality ()
#7 0x00007d3c in Lib::Environment::Environment ()
#8 0x000080f4 in __static_initialization_and_destruction_0 ()
#9 0x00008144 in _GLOBAL__sub_I_Environment.cpp ()
#10 0x8fe15d60 in __dyld__ZN16ImageLoaderMachO16doInitializationERKN11ImageLoader11LinkContextE ()
#11 0x8fe0f70c in __dyld__ZN11ImageLoader23recursiveInitializationERKNS_11LinkContextEj ()
#12 0x8fe0f804 in __dyld__ZN11ImageLoader15runInitializersERKNS_11LinkContextE ()
#13 0x8fe02708 in __dyld__ZN4dyld24initializeMainExecutableEv ()
#14 0x8fe08690 in __dyld__ZN4dyld5_mainEPK11mach_headermiPPKcS5_S5_ ()
#15 0x8fe017cc in __dyld__ZN13dyldbootstrap5startEPK11mach_headeriPPKcl ()
#16 0x8fe01064 in __dyld__dyld_start ()
barracuda156 commented
@MichaelRawson This seems to be nothing specific to either macOS or powerpc, but rather broken 32-bit support. Could this be addressed? If it is just a 32-bit issue, it should be reproducible on Linux on i386, for example.
MichaelRawson commented
OK, thanks for investigating - in principle there's no reason we couldn't support 32-bit platforms, but none of us currently use a 32-bit machine (I think). We do some gross stuff with memory (mostly term layout) that is probably the source of that particular crash. I'm cross-compiling now for i386 and working out some of the bugs.
MichaelRawson commented
(moving conversation back here, no longer "just" a 32-bit arch problem)
Thanks for testing! 4-byte bool should be OK, spinlock...no idea, we don't use them explicitly.
Big endian
Uh-oh. Showing my PowerPC ignorance here, I didn't know this. I expect this is (another) source of bugs with the term representation, then.
However, the existence of the port suggests this worked (miraculously) at some point. Would you be able to bisect this and work out which commit broke PowerPC?
barracuda156 commented
@MichaelRawson Well, existence of port only means it has built at the time (but it also builds now). Whether it ever actually worked is an open question.
So I don’t really know how to bisect it in such a case: it is not realistically feasible to build and run tests for each commit when we have no idea if it ever worked.
I could certainly try a couple of somewhat old versions though just to get an idea.
We could get some extra info from GDB, like registers state, but we needs someone understanding low-level ABI to make sense of that, perhaps.
Given that the build works with no hackery, I suspect the issue is either bitness or endianness or a consequence of assuming 1-byte bools (the latter is sometimes not obvious).
If you have any suspicion what parts of the code may be relevant, please point to them.
I can test this on i386 macOS in a while (to see if 32-bitness specifically on MacOS matters) and possibly ppc64 (which has 1-byte bools, so only endianness is an issue).
MichaelRawson commented
Whether it ever actually worked is an open question.
True!
So I don’t really know how to bisect it in such a case: it is not realistically feasible to build and run tests for each commit when we have no idea if it ever worked.
Sure; I was going off the metadata at https://github.com/macports/macports-ports/blob/c7df747729c62f2801614020663ef140a33663e1/math/vampire/Portfile#L11 which suggests commit 1f1a9d99e4f6ca018dc3e9af05c49fb1d337a9bd is used there. If I'm reading that right, could you check that commit?
In the event that this commit works, it's only a couple of years old, so git bisect estimates 9 build/compile/crash steps, if that seems more realistic.
If you have any suspicion what parts of the code may be relevant, please point to them.
I'm almost certain it's TermList in Kernel/Term.hpp, specifically the pointer tagging we use here:
Line 224 in 31939a4
The comment block above is quite funny in this context! Anyhow, if you move that field to the end of the bitfield, after id, I suspect it might work. If that's the case, we can think about a proper fix.
As far as I'm aware this is the least-portable part of Vampire. There might be others, but I'd look here first. We are generally trying to improve the portability situation, so thank you for bringing this to our attention.
barracuda156 commented
So I tried modifying the struct there like this:
struct {
/** polarity, used only for literals */
unsigned polarity : 1;
/** true if commutative/symmetric */
unsigned commutative : 1;
/** true if shared */
unsigned shared : 1;
/** true if literal */
unsigned literal : 1;
/** true if atomic sort */
unsigned sort : 1;
/** true if term contains at least one term var */
unsigned hasTermVar : 1;
/** Ordering comparison result for commutative term arguments, one of
* 0 (unknown) 1 (less), 2 (equal), 3 (greater), 4 (incomparable)
* @see Term::ArgumentOrder */
unsigned order : 3;
static_assert(AO_INCOMPARABLE < 8, "must be able to squash this into 3 bits");
/** Number of distinct variables in the term, equal
* to TERM_DIST_VAR_UNKNOWN if the number has not been
* computed yet. */
mutable unsigned distinctVars : TERM_DIST_VAR_BITS;
/** term id hiding in this _info */
// this should not be removed without care,
// otherwise the bitfield layout might shift, resulting in broken pointer tagging
unsigned id : 32;
/** a TermTag indicating what is stored here */
unsigned tag : 2;
} _info;
};
Build failed then:
In file included from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Debug/TimeProfiling.hpp:19,
from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Lib/Metaiterators.hpp:29,
from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Lib/Set.hpp:26,
from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Indexing/TermSharing.hpp:20,
from /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Lib/Environment.cpp:20:
/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Kernel/Term.hpp:269:32: error: static assertion failed: size of TermList must be exactly 64 bits
269 | static_assert(sizeof(TermList) == 8, "size of TermList must be exactly 64 bits");
| ~~~~~~~~~~~~~~~~~^~~~
/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Kernel/Term.hpp:269:32: note: the comparison reduces to '(16 == 8)'
ninja: build stopped: subcommand failed.
barracuda156 commented
Just in case, I removed the assert and completed the build. The binary now crashes differently:
36-184% /opt/local/bin/vampire
Condition tag() == REF in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Kernel/Term.hpp, line 103 was violated, as:
tag() == 2
REF == 0
----- stack dump -----
Version : Vampire 4.8 (commit )
???
???
???
???
???
???
???
Lib::Environment::Environment()
Kernel::Signature::addEquality()
Kernel::OperatorType::getPredicateType(unsigned int, Kernel::TermList const*, unsigned int)
Kernel::OperatorType::setupKey(unsigned int, Kernel::TermList const*)
Kernel::AtomicSort::defaultSort()
Kernel::Signature::getDefaultSort()
Kernel::AtomicSort::superSort()
Kernel::TermList::TermList(Kernel::Term*)
void Debug::Assertion::violatedEquality<Kernel::TermTag, Kernel::TermTag>(char const*, int, char const*, char const*, Kernel::TermTag const&, Kernel::TermTag const&)
Debug::Tracer::printStack(std::ostream&)
----- end of stack dump -----
MichaelRawson commented
So I tried modifying the struct there like this:
Build failed
static assertion failed: size of TermList must be exactly 64 bits
note: the comparison reduces to '(16 == 8)'
Looks like compiler padding broke us, and if TermList is not the size we expect it to be even more will break, as you found. I managed to fix it for ppc64 by putting id first, see https://godbolt.org/z/fb955shdo
Would you be willing to test this approach? Sorry about the extra cycle, I should have tried myself first. If it works (or at least crashes less) I can think about how to fix it properly.
barracuda156 commented
@MichaelRawson This worked!
Only few tests fail:
[0/1] Running tests...
Test project /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
Start 1: DHMap
1/34 Test #1: DHMap ............................. Passed 0.18 sec
Start 2: QuotientE
2/34 Test #2: QuotientE ......................... Passed 0.40 sec
Start 3: UnificationWithAbstraction
3/34 Test #3: UnificationWithAbstraction ........ Passed 0.14 sec
Start 4: GaussianElimination
4/34 Test #4: GaussianElimination ............... Passed 0.50 sec
Start 5: PushUnaryMinus
5/34 Test #5: PushUnaryMinus .................... Passed 0.15 sec
Start 6: ArithmeticSubtermGeneralization
6/34 Test #6: ArithmeticSubtermGeneralization ... Passed 4.28 sec
Start 7: InterpretedFunctions
7/34 Test #7: InterpretedFunctions .............. Passed 5.98 sec
Start 8: Rebalance
8/34 Test #8: Rebalance ......................... Passed 0.90 sec
Start 9: Disagreement
9/34 Test #9: Disagreement ...................... Passed 0.12 sec
Start 10: DynamicHeap
10/34 Test #10: DynamicHeap ....................... Passed 0.12 sec
Start 11: Induction
11/34 Test #11: Induction ......................... Passed 2.46 sec
Start 12: IntegerConstantType
12/34 Test #12: IntegerConstantType ............... Passed 0.09 sec
Start 13: SATSolver
13/34 Test #13: SATSolver ......................... Passed 0.11 sec
Start 14: ArithCompare
14/34 Test #14: ArithCompare ...................... Passed 0.09 sec
Start 15: SyntaxSugar
15/34 Test #15: SyntaxSugar ....................... Passed 0.16 sec
Start 16: SkipList
16/34 Test #16: SkipList .......................... Passed 1.20 sec
Start 17: BinaryHeap
17/34 Test #17: BinaryHeap ........................ Passed 0.09 sec
Start 18: SafeRecursion
18/34 Test #18: SafeRecursion ..................... Passed 0.09 sec
Start 19: KBO
19/34 Test #19: KBO ............................... Passed 0.55 sec
Start 20: SKIKBO
20/34 Test #20: SKIKBO ............................ Passed 0.16 sec
Start 21: LPO
21/34 Test #21: LPO ............................... Passed 0.14 sec
Start 22: RatioKeeper
22/34 Test #22: RatioKeeper ....................... Passed 0.09 sec
Start 23: TwoVampires
23/34 Test #23: TwoVampires .......................***Timeout 20.11 sec
Start 24: OptionConstraints
24/34 Test #24: OptionConstraints ................. Passed 0.30 sec
Start 25: DHMultiset
25/34 Test #25: DHMultiset ........................ Passed 0.22 sec
Start 26: List
26/34 Test #26: List .............................. Passed 0.09 sec
Start 27: BottomUpEvaluation
27/34 Test #27: BottomUpEvaluation ................ Passed 0.10 sec
Start 28: Coproduct
28/34 Test #28: Coproduct ......................... Passed 0.14 sec
Start 29: EqualityResolution
29/34 Test #29: EqualityResolution ................ Passed 0.30 sec
Start 30: Iterator
30/34 Test #30: Iterator .......................... Passed 0.11 sec
Start 31: Option
31/34 Test #31: Option ............................ Passed 0.11 sec
Start 32: Stack
32/34 Test #32: Stack ............................. Passed 0.08 sec
Start 33: TheoryInstAndSimp
33/34 Test #33: TheoryInstAndSimp .................***Failed 9.76 sec
Start 34: Z3Interfacing
34/34 Test #34: Z3Interfacing ..................... Passed 3.29 sec
94% tests passed, 2 tests failed out of 34
Total Test time (real) = 52.66 sec
Here is the output:
23/34 Testing: TwoVampires
23/34 Test: TwoVampires
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "TwoVampires"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"TwoVampires" start time: Dec 18 19:27 CST
Output:
----------------------------------------------------------
Running two_vampires1...
dis+4_8_30 on
User error: option spl not known
<end of output>
Test time = 20.11 sec
----------------------------------------------------------
Test Failed.
33/34 Testing: TheoryInstAndSimp
33/34 Test: TheoryInstAndSimp
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "TheoryInstAndSimp"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"TheoryInstAndSimp" start time: Dec 18 19:28 CST
Output:
----------------------------------------------------------
Running test_01...
[ OK ] test_01
Running test_02...
[ OK ] test_02
Running test_03...
[ OK ] test_03
Running test_04...
[ OK ] test_04
Running test_05...
[ OK ] test_05
Running test_06...
[ OK ] test_06
Running test_07...
[ OK ] test_07
Running test_08...
[ OK ] test_08
Running test_09...
[ OK ] test_09
Running test_all_vs_strong_1a...
[ OK ] test_all_vs_strong_1a
Running test_all_vs_strong_1b...
[ OK ] test_all_vs_strong_1b
Running test_all_vs_strong_2a...
[ OK ] test_all_vs_strong_2a
Running test_all_vs_strong_2b...
[ OK ] test_all_vs_strong_2b
Running test_overlap_vs_strong_1a...
[ OK ] test_overlap_vs_strong_1a
Running test_overlap_vs_strong_1b...
[ OK ] test_overlap_vs_strong_1b
Running test_overlap_vs_strong_2...
[ OK ] test_overlap_vs_strong_2
Running bug_01...
[ OK ] bug_01
Running bug_02...
[ OK ] bug_02
Running bug_03...
[ OK ] bug_03
Running bug_04...
[ OK ] bug_04
Running pair_1...
[ OK ] pair_1
Running generalisation_1... Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
start
main
Test::UnitTesting::run(Lib::Stack<std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > > const&)
Test::UnitTesting::runUnit(std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > const&)
Test::TestUnit::run(std::ostream&)
Test::TestUnit::spawnTest(void (*)())
__testFn__TheoryInstAndSimp__generalisation_1()
void Test::Generation::TestCase::run<Inferences::TheoryInstAndSimp>(Test::Generation::GenerationTester<Inferences::TheoryInstAndSimp>&)
Inferences::TheoryInstAndSimp::generateSimplify(Kernel::Clause*)
Inferences::TheoryInstAndSimp::getSolutions(Lib::Stack<Kernel::Literal*> const&, Lib::Stack<Kernel::Literal*> const&, unsigned int)
Inferences::TheoryInstAndSimp::instantiateGeneralised(Inferences::TheoryInstAndSimp::SkolemizedLiterals, unsigned int)
void Debug::Assertion::violatedEquality<SAT::SATSolver::Status, SAT::SATSolver::Status>(char const*, int, char const*, char const*, SAT::SATSolver::Status const&, SAT::SATSolver::Status const&)
Debug::Tracer::printStack(std::ostream&)
[ FAIL ] generalisation_1
Running generalisation_2... Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
start
main
Test::UnitTesting::run(Lib::Stack<std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > > const&)
Test::UnitTesting::runUnit(std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > const&)
Test::TestUnit::run(std::ostream&)
Test::TestUnit::spawnTest(void (*)())
__testFn__TheoryInstAndSimp__generalisation_2()
void Test::Generation::TestCase::run<Inferences::TheoryInstAndSimp>(Test::Generation::GenerationTester<Inferences::TheoryInstAndSimp>&)
Inferences::TheoryInstAndSimp::generateSimplify(Kernel::Clause*)
Inferences::TheoryInstAndSimp::getSolutions(Lib::Stack<Kernel::Literal*> const&, Lib::Stack<Kernel::Literal*> const&, unsigned int)
Inferences::TheoryInstAndSimp::instantiateGeneralised(Inferences::TheoryInstAndSimp::SkolemizedLiterals, unsigned int)
void Debug::Assertion::violatedEquality<SAT::SATSolver::Status, SAT::SATSolver::Status>(char const*, int, char const*, char const*, SAT::SATSolver::Status const&, SAT::SATSolver::Status const&)
Debug::Tracer::printStack(std::ostream&)
[ FAIL ] generalisation_2
Running generalisation_3... Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
start
main
Test::UnitTesting::run(Lib::Stack<std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > > const&)
Test::UnitTesting::runUnit(std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > const&)
Test::TestUnit::run(std::ostream&)
Test::TestUnit::spawnTest(void (*)())
__testFn__TheoryInstAndSimp__generalisation_3()
void Test::Generation::TestCase::run<Inferences::TheoryInstAndSimp>(Test::Generation::GenerationTester<Inferences::TheoryInstAndSimp>&)
Inferences::TheoryInstAndSimp::generateSimplify(Kernel::Clause*)
Inferences::TheoryInstAndSimp::getSolutions(Lib::Stack<Kernel::Literal*> const&, Lib::Stack<Kernel::Literal*> const&, unsigned int)
Inferences::TheoryInstAndSimp::instantiateGeneralised(Inferences::TheoryInstAndSimp::SkolemizedLiterals, unsigned int)
void Debug::Assertion::violatedEquality<SAT::SATSolver::Status, SAT::SATSolver::Status>(char const*, int, char const*, char const*, SAT::SATSolver::Status const&, SAT::SATSolver::Status const&)
Debug::Tracer::printStack(std::ostream&)
[ FAIL ] generalisation_3
Running generalisation_4... Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
start
main
Test::UnitTesting::run(Lib::Stack<std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > > const&)
Test::UnitTesting::runUnit(std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > const&)
Test::TestUnit::run(std::ostream&)
Test::TestUnit::spawnTest(void (*)())
__testFn__TheoryInstAndSimp__generalisation_4()
void Test::Generation::TestCase::run<Inferences::TheoryInstAndSimp>(Test::Generation::GenerationTester<Inferences::TheoryInstAndSimp>&)
Inferences::TheoryInstAndSimp::generateSimplify(Kernel::Clause*)
Inferences::TheoryInstAndSimp::getSolutions(Lib::Stack<Kernel::Literal*> const&, Lib::Stack<Kernel::Literal*> const&, unsigned int)
Inferences::TheoryInstAndSimp::instantiateGeneralised(Inferences::TheoryInstAndSimp::SkolemizedLiterals, unsigned int)
void Debug::Assertion::violatedEquality<SAT::SATSolver::Status, SAT::SATSolver::Status>(char const*, int, char const*, char const*, SAT::SATSolver::Status const&, SAT::SATSolver::Status const&)
Debug::Tracer::printStack(std::ostream&)
[ FAIL ] generalisation_4
Running generalisation_5... Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-459694c831f812ed5ecbe14ea15a32d78a095ed7/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
start
main
Test::UnitTesting::run(Lib::Stack<std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > > const&)
Test::UnitTesting::runUnit(std::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > const&)
Test::TestUnit::run(std::ostream&)
Test::TestUnit::spawnTest(void (*)())
__testFn__TheoryInstAndSimp__generalisation_5()
void Test::Generation::TestCase::run<Inferences::TheoryInstAndSimp>(Test::Generation::GenerationTester<Inferences::TheoryInstAndSimp>&)
Inferences::TheoryInstAndSimp::generateSimplify(Kernel::Clause*)
Inferences::TheoryInstAndSimp::getSolutions(Lib::Stack<Kernel::Literal*> const&, Lib::Stack<Kernel::Literal*> const&, unsigned int)
Inferences::TheoryInstAndSimp::instantiateGeneralised(Inferences::TheoryInstAndSimp::SkolemizedLiterals, unsigned int)
void Debug::Assertion::violatedEquality<SAT::SATSolver::Status, SAT::SATSolver::Status>(char const*, int, char const*, char const*, SAT::SATSolver::Status const&, SAT::SATSolver::Status const&)
Debug::Tracer::printStack(std::ostream&)
[ FAIL ] generalisation_5
Tests run: 26
- ok 21 (80.8) %
- fail 5 (19.2) %
<end of output>
Test time = 9.76 sec
----------------------------------------------------------
Test Failed.
barracuda156 commented
@MichaelRawson If we could incorporate a fix for Big-endian platforms into the code, that would be awesome.
Re tests, can these two failures be fixed?
MichaelRawson commented
I'm glad it "worked" - looks like we crash a bit less now. :-) A proper fix is now top of my Vampire list, probably end of the week or so.
The failures are still a bit concerning. TwoVampires is an old test of probably limited value that launches two separate instances - apparently one with an option we don't have any more. It's interesting that it fails on your machine, though - I think it passes for others, which is why it hasn't been fixed yet. Would you be able to step through control-flow on your machine in a debugger and figure out how it fails?
The TheoryInstAndSimp failures look a bit more like a straight-up bug to me, rather than a flaky test. I don't know that part of the code very well - @joe-hauns do you know what might be causing your tests to fail on a big-endian architecture? Bit-stuffing in Coproduct or something like this?
MichaelRawson commented
Spoke to @joe-hauns earlier. The tests are failing because the Z3 SMT solver returns sat rather than unsat, which should never happen. This could be because:
- Vampire is still buggy on PowerPC somehow and produces a satisfiable problem for Z3 to chew on.
- Z3 is also broken on PowerPC.
If it's (1), then we should investigate. If it's (2) we should file a bug with Z3. To work it out, could you change this line to true and see what gets output? It may also be helpful to change the string two lines below, which is a path that the relevant SMT problem gets dumped to.
barracuda156 commented
@MichaelRawson Sorry for a ridiculous delay, I am back to the issue now.
Just in case, is Big-endian support incorporated into the master or should I resort to local patching for now?
MichaelRawson commented
Hey, no problem, I'm just getting back to it too. :-)
Just in case, is Big-endian support incorporated into the master or should I resort to local patching for now?
Unfortunately not - I have a fix planned for the Term endianness, but now there's a huge PR coming in which I want to get merged first. Hopefully this week! In the meantime, could you look at the Z3 bug above? I think that ought to be independent of Term.
barracuda156 commented
@MichaelRawson I rebuilt and ran tests from master (with a patch to Temp). Overall results did not change:
94% tests passed, 2 tests failed out of 35
Total Test time (real) = 48.27 sec
The following tests FAILED:
23 - TwoVampires (Timeout)
34 - TheoryInstAndSimp (Failed)
Is this helpful for Z3 issue?
34/35 Testing: TheoryInstAndSimp
34/35 Test: TheoryInstAndSimp
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "TheoryInstAndSimp"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"TheoryInstAndSimp" start time: Jan 16 08:48 CST
Output:
----------------------------------------------------------
Running test_01... [Z3] solve result: sat
[Z3] add (naming): (= v4 (< |c'$inst0'| |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v3 (< 0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 6 (* |c'$inst0'| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 1 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_01
Running test_02... [Z3] solve result: sat
[Z3] add (naming): (= v5 ((_ is cons) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v6 ((_ is cons) |c'$inst2'|))
[Z3] solve result: sat
[Z3] add (naming): (= v5 ((_ is cons) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v6 ((_ is cons) |c'$inst2'|))
[Z3] solve result: sat
[Z3] add (naming): (= v5 ((_ is cons) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v4 (= nil (|'cons@1'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v3 (= 1 (|'cons@0'_$| |c'$inst2'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 0 (|'cons@0'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= (|'cons@1'_$| |c'$inst1'|) (|'cons@1'_$| |c'$inst2'|)))
[Z3] solve result: sat
[ OK ] test_02
Running test_03...
[ OK ] test_03
Running test_04...
[ OK ] test_04
Running test_05... [Z3] solve result: sat
[Z3] add (naming): (= v2 (= 7.0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0.0 (+ |c'$inst0'| |c'$inst1'|)))
[Z3] solve result: sat
[ OK ] test_05
Running test_06... [Z3] solve result: sat
[Z3] add (naming): (= v2 (= 7.0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= (+ |c'$inst0'| |c'$inst1'|) (* 0.0 |c'$inst2'|)))
[Z3] solve result: sat
[ OK ] test_06
Running test_07... [Z3] solve result: sat
[Z3] add (naming): (= v2 (= 7.0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= (+ |c'$inst0'| |c'$inst1'|) (* 0.0 |c'$inst2'|)))
[Z3] solve result: sat
[ OK ] test_07
Running test_08... [Z3] solve result: sat
[Z3] add (naming): (= v3 (= 1 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 1))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_08
Running test_09... [Z3] solve result: sat
[Z3] add (naming): (= v3 (= 0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 1))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_09
Running test_all_vs_strong_1a... [Z3] solve result: sat
[Z3] add (naming): (= v2 (< |c'$inst0'| 1))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (< (- 1) |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_all_vs_strong_1a
Running test_all_vs_strong_1b... [Z3] solve result: sat
[Z3] add (naming): (= v3 (= 0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (< |c'$inst0'| 1))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (< (- 1) |c'$inst0'|))
[Z3] solve result: unsat
[ OK ] test_all_vs_strong_1b
Running test_all_vs_strong_2a... [Z3] solve result: sat
[Z3] add (naming): (= v1 (= 7 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_all_vs_strong_2a
Running test_all_vs_strong_2b... [Z3] solve result: sat
[Z3] add (naming): (= v1 (= 7 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 7 |c'$inst0'|))
[Z3] solve result: unsat
[ OK ] test_all_vs_strong_2b
Running test_overlap_vs_strong_1a... [Z3] solve result: sat
[Z3] add (naming): (= v3 (= 0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 0))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: unsat
[ OK ] test_overlap_vs_strong_1a
Running test_overlap_vs_strong_1b... [Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 0))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_overlap_vs_strong_1b
Running test_overlap_vs_strong_2... [Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 0))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_overlap_vs_strong_2
Running bug_01... [Z3] solve result: sat
[Z3] add (naming): (= v2 ((_ is pair) (pair 0 127)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0 (|'pair@0'_$| (pair 0 127))))
[Z3] solve result: unsat
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0 (|'pair@0'_$| (pair 0 127))))
[Z3] solve result: unsat
[ OK ] bug_01
Running bug_02... [Z3] solve result: sat
[Z3] add (naming): (= v2 ((_ is cons) nil))
[Z3] solve result: unsat
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= nil (|'cons@1'_$| nil)))
[Z3] solve result: sat
[ OK ] bug_02
Running bug_03... [Z3] solve result: sat
[Z3] add (naming): (= v2 ((_ is pair) (pair 0 127)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0 (|'pair@0'_$| (pair 0 127))))
[Z3] solve result: sat
[ OK ] bug_03
Running bug_04... [Z3] add (naming): (= v1 (= nil (|'cons@1'_$| nil)))
[Z3] add (naming): (= v2 ((_ is cons) nil))
[Z3] solve result: unsat
[Z3] add (naming): (= v1 (= nil (|'cons@1'_$| nil)))
[Z3] solve result: sat
[ OK ] bug_04
Running pair_1... [Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 10 (|'pair@0'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0 (+ (|'pair@0'_$| |c'$inst1'|) (|'pair@1'_$| |c'$inst1'|))))
[Z3] solve result: sat
[ OK ] pair_1
Running generalisation_1... [Z3] add (naming): (= v1 (= 10 (|'pair@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (clause): (or false v0 v3)
[Z3] add (naming): (= v3 (= 10 |c'$inst$gen2'|))
[Z3] add (naming): (= v4 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v5 (= |c'$inst1'| (pair |c'$inst$gen2'| |c'$inst$gen3'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3efc36910da44cc6b95b660baa7ce60b397d1e91/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x10ee70 0x9931c4 0x9925fc 0x9927c4 0x992a68 0x992e9c 0x2e83f0 0x2eb400 0x6177ec 0x615790 0x61542c 0x618374 0x6150b0 0x2a22ac 0x3657c
[ FAIL ] generalisation_1
Running generalisation_2... [Z3] add (naming): (let ((a!1 (= 10
(+ (|'cons@0'_$| |c'$inst1'|)
(|'cons@0'_$| (|'cons@1'_$| |c'$inst1'|))))))
(= v1 a!1))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v3 ((_ is cons) |c'$inst1'|))
[Z3] add (naming): (= v4 ((_ is cons) (|'cons@1'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is cons) |c'$inst1'|))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (clause): (or false v0 v3 v2 v5 v2 v2)
[Z3] add (naming): (= v5 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v6 (= 8 |c'$inst$gen5'|))
[Z3] add (naming): (= v7 (= nil |c'$inst$gen6'|))
[Z3] add (naming): (= v8 (= |c'$inst$gen4'| (cons |c'$inst$gen5'| |c'$inst$gen6'|)))
[Z3] add (naming): (= v9 (= |c'$inst1'| (cons |c'$inst$gen3'| |c'$inst$gen4'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3efc36910da44cc6b95b660baa7ce60b397d1e91/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x10ee70 0x9931c4 0x9925fc 0x9927c4 0x992a68 0x992e9c 0x2e8d2c 0x2eb400 0x6177ec 0x615790 0x61542c 0x618374 0x6150b0 0x2a22ac 0x3657c
[ FAIL ] generalisation_2
Running generalisation_3... [Z3] add (naming): (let ((a!1 (+ (|'cons@0'_$| |c'$inst1'|)
(|'cons@0'_$| (|'cons@1'_$| (|'cons@1'_$| |c'$inst1'|))))))
(= v1 (= 10 a!1)))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v3 ((_ is cons) |c'$inst1'|))
[Z3] add (naming): (= v4 ((_ is cons) (|'cons@1'_$| (|'cons@1'_$| |c'$inst1'|))))
[Z3] add (naming): (= v5 ((_ is cons) (|'cons@1'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is cons) |c'$inst1'|))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v5 ((_ is cons) (|'cons@1'_$| |c'$inst1'|)))
[Z3] add (naming): (= v4 ((_ is cons) (|'cons@1'_$| (|'cons@1'_$| |c'$inst1'|))))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (clause): (or false v0 v3 v2 v5 v4 v2 v2)
[Z3] add (naming): (= v6 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v7 (= 3 |c'$inst$gen5'|))
[Z3] add (naming): (= v8 (= 8 |c'$inst$gen7'|))
[Z3] add (naming): (= v9 (= nil |c'$inst$gen8'|))
[Z3] add (naming): (= v10 (= |c'$inst$gen6'| (cons |c'$inst$gen7'| |c'$inst$gen8'|)))
[Z3] add (naming): (= v11 (= |c'$inst$gen4'| (cons |c'$inst$gen5'| |c'$inst$gen6'|)))
[Z3] add (naming): (= v12 (= |c'$inst1'| (cons |c'$inst$gen3'| |c'$inst$gen4'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3efc36910da44cc6b95b660baa7ce60b397d1e91/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x10ee70 0x9931c4 0x9925fc 0x9927c4 0x992a68 0x992e9c 0x2e9798 0x2eb400 0x6177ec 0x615790 0x61542c 0x618374 0x6150b0 0x2a22ac 0x3657c
[ FAIL ] generalisation_3
Running generalisation_4... [Z3] add (naming): (= v1 (= nil (|'cons@1'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 ((_ is cons) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (clause): (or false (not v0) v3)
[Z3] add (naming): (= v3 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v4 (= 3 |c'$inst$gen5'|))
[Z3] add (naming): (= v5 (= nil |c'$inst$gen6'|))
[Z3] add (naming): (= v6 (= |c'$inst$gen4'| (cons |c'$inst$gen5'| |c'$inst$gen6'|)))
[Z3] add (naming): (= v7 (= |c'$inst1'| (cons |c'$inst$gen3'| |c'$inst$gen4'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3efc36910da44cc6b95b660baa7ce60b397d1e91/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x10ee70 0x9931c4 0x9925fc 0x9927c4 0x992a68 0x992e9c 0x2ea11c 0x2eb400 0x6177ec 0x615790 0x61542c 0x618374 0x6150b0 0x2a22ac 0x3657c
[ FAIL ] generalisation_4
Running generalisation_5... [Z3] add (naming): (= v1 (= zero (|'s@0'_$| (|'s@0'_$| |c'$inst1'|))))
[Z3] add (naming): (= v2 ((_ is s) (|'s@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v3 ((_ is s) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is s) |c'$inst1'|))
[Z3] add (naming): (= v2 ((_ is s) (|'s@0'_$| |c'$inst1'|)))
[Z3] add (clause): (or false (not v0) v3 v2)
[Z3] add (naming): (= v4 (= zero |c'$inst$gen5'|))
[Z3] add (naming): (= v5 (= |c'$inst$gen4'| (s |c'$inst$gen5'|)))
[Z3] add (naming): (= v6 (= |c'$inst$gen3'| (s |c'$inst$gen4'|)))
[Z3] add (naming): (= v7 (= |c'$inst1'| (s |c'$inst$gen3'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-3efc36910da44cc6b95b660baa7ce60b397d1e91/Inferences/TheoryInstAndSimp.cpp, line 569 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x10ee70 0x9931c4 0x9925fc 0x9927c4 0x992a68 0x992e9c 0x2ea89c 0x2eb400 0x6177ec 0x615790 0x61542c 0x618374 0x6150b0 0x2a22ac 0x3657c
[ FAIL ] generalisation_5
Tests run: 26
- ok 21 (80.8) %
- fail 5 (19.2) %
<end of output>
Test time = 7.47 sec
----------------------------------------------------------
Test Failed.
"TheoryInstAndSimp" end time: Jan 16 08:48 CST
"TheoryInstAndSimp" time elapsed: 00:00:07
MichaelRawson commented
OK, on my (x86_64 )machine for e.g. generalisation_01 I get
Running generalisation_1... [Z3] add (naming): (= v1 (= 10 (|'pair@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 10 (|'pair@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 ((_ is pair) |c'$inst1'|))
[Z3] add (clause): (or false (not v1) (not v2))
[Z3] add (naming): (= v3 (= 10 |c'$inst$gen2'|))
[Z3] add (naming): (= v4 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v5 (= |c'$inst1'| (pair |c'$inst$gen2'| |c'$inst$gen3'|)))
[Z3] solve result: unsat
So there's something going wrong on the Vampire side. I'll fix the term representation first and we can investigate this later.
barracuda156 commented
@MichaelRawson Great, just ping me when to test it again.
barracuda156 commented
@MichaelRawson Hi, any update on this? Should we return to testing?
MichaelRawson commented
Hi! #524 ought to be a "proper fix" for at least the TermList bitfield - if you're willing to test that branch I'd appreciate it. I doubt it fixes the above bug (maybe it's something in Z3?), but you never know...
After (if) that's merged we can investigate further. Thanks for persisting.
barracuda156 commented
@MichaelRawson Sure, will test in a couple of days, likely tomorrow.
barracuda156 commented
@MichaelRawson Building from 4455f14 (we also updated z3 to 4.12.6):
---> Testing vampire
Executing: cd "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build" && ninja test
[0/1] Running tests...
Test project /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
Start 1: DHMap
1/38 Test #1: DHMap ............................. Passed 0.19 sec
Start 2: QuotientE
2/38 Test #2: QuotientE ......................... Passed 0.47 sec
Start 3: UnificationWithAbstraction
3/38 Test #3: UnificationWithAbstraction ........ Passed 1.99 sec
Start 4: GaussianElimination
4/38 Test #4: GaussianElimination ............... Passed 0.67 sec
Start 5: PushUnaryMinus
5/38 Test #5: PushUnaryMinus .................... Passed 0.21 sec
Start 6: ArithmeticSubtermGeneralization
6/38 Test #6: ArithmeticSubtermGeneralization ... Passed 5.93 sec
Start 7: InterpretedFunctions
7/38 Test #7: InterpretedFunctions .............. Passed 9.04 sec
Start 8: Rebalance
8/38 Test #8: Rebalance ......................... Passed 1.39 sec
Start 9: Disagreement
9/38 Test #9: Disagreement ...................... Passed 0.11 sec
Start 10: DynamicHeap
10/38 Test #10: DynamicHeap ....................... Passed 0.17 sec
Start 11: Induction
11/38 Test #11: Induction ......................... Passed 3.95 sec
Start 12: IntegerConstantType
12/38 Test #12: IntegerConstantType ............... Passed 0.11 sec
Start 13: SATSolver
13/38 Test #13: SATSolver ......................... Passed 0.15 sec
Start 14: ArithCompare
14/38 Test #14: ArithCompare ...................... Passed 0.10 sec
Start 15: SyntaxSugar
15/38 Test #15: SyntaxSugar ....................... Passed 0.26 sec
Start 16: SkipList
16/38 Test #16: SkipList .......................... Passed 1.05 sec
Start 17: BinaryHeap
17/38 Test #17: BinaryHeap ........................ Passed 0.12 sec
Start 18: SafeRecursion
18/38 Test #18: SafeRecursion ..................... Passed 0.12 sec
Start 19: KBO
19/38 Test #19: KBO ............................... Passed 0.82 sec
Start 20: SKIKBO
20/38 Test #20: SKIKBO ............................ Passed 0.23 sec
Start 21: LPO
21/38 Test #21: LPO ............................... Passed 0.19 sec
Start 22: RatioKeeper
22/38 Test #22: RatioKeeper ....................... Passed 0.11 sec
Start 23: OptionConstraints
23/38 Test #23: OptionConstraints ................. Passed 0.27 sec
Start 24: DHMultiset
24/38 Test #24: DHMultiset ........................ Passed 0.21 sec
Start 25: List
25/38 Test #25: List .............................. Passed 0.10 sec
Start 26: BottomUpEvaluation
26/38 Test #26: BottomUpEvaluation ................ Passed 0.13 sec
Start 27: Coproduct
27/38 Test #27: Coproduct ......................... Passed 0.30 sec
Start 28: EqualityResolution
28/38 Test #28: EqualityResolution ................ Passed 0.36 sec
Start 29: Iterator
29/38 Test #29: Iterator .......................... Passed 0.21 sec
Start 30: Option
30/38 Test #30: Option ............................ Passed 0.25 sec
Start 31: Stack
31/38 Test #31: Stack ............................. Passed 0.11 sec
Start 32: Set
32/38 Test #32: Set ............................... Passed 0.14 sec
Start 33: Deque
33/38 Test #33: Deque ............................. Passed 0.12 sec
Start 34: TermAlgebra
34/38 Test #34: TermAlgebra ....................... Passed 0.14 sec
Start 35: FunctionDefinitionHandler
35/38 Test #35: FunctionDefinitionHandler ......... Passed 0.39 sec
Start 36: FunctionDefinitionRewriting
36/38 Test #36: FunctionDefinitionRewriting ....... Passed 0.50 sec
Start 37: TheoryInstAndSimp
37/38 Test #37: TheoryInstAndSimp .................***Failed 7.81 sec
Start 38: Z3Interfacing
38/38 Test #38: Z3Interfacing ..................... Passed 3.20 sec
97% tests passed, 1 tests failed out of 38
Total Test time (real) = 41.68 sec
The following tests FAILED:
37 - TheoryInstAndSimp (Failed)
Errors while running CTest
Is /usr/bin/atos anything consequential? For some reason it is not allowed:
Start testing: Mar 19 03:04 CST
----------------------------------------------------------
1/38 Testing: DHMap
1/38 Test: DHMap
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "DHMap"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"DHMap" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running dhmap1...
[ OK ] dhmap1
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.36 sec
----------------------------------------------------------
Test Passed.
"DHMap" end time: Mar 19 03:04 CST
"DHMap" time elapsed: 00:00:00
----------------------------------------------------------
2/38 Testing: QuotientE
2/38 Test: QuotientE
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "QuotientE"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"QuotientE" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running check_spec...
[ OK ] check_spec
Running check_int...
[ OK ] check_int
Running check_ceiling_RationalConstantType...
[ OK ] check_ceiling_RationalConstantType
Running check_floor_RationalConstantType...
[ OK ] check_floor_RationalConstantType
Running check_ceiling_RealConstantType...
[ OK ] check_ceiling_RealConstantType
Running check_floor_RealConstantType...
[ OK ] check_floor_RealConstantType
Tests run: 6
- ok 6 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.48 sec
----------------------------------------------------------
Test Passed.
"QuotientE" end time: Mar 19 03:04 CST
"QuotientE" time elapsed: 00:00:00
----------------------------------------------------------
3/38 Testing: UnificationWithAbstraction
3/38 Test: UnificationWithAbstraction
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "UnificationWithAbstraction"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"UnificationWithAbstraction" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running term_indexing_one_side_interp_01...
[ OK ] f(X0): $int
[ OK ] term_indexing_one_side_interp_01
Running term_indexing_one_side_interp_02...
[ OK ] g(X0): $int
[ OK ] term_indexing_one_side_interp_02
Running term_indexing_one_side_interp_03...
[ OK ] X0: $int
[ OK ] term_indexing_one_side_interp_03
Running term_indexing_one_side_interp_04...
[ OK ] $sum(b,2): $int
[ OK ] term_indexing_one_side_interp_04
Running term_indexing_one_side_interp_04_b...
[ OK ] $sum(2,a): $int
[ OK ] term_indexing_one_side_interp_04_b
Running term_indexing_one_side_interp_04_c...
[ OK ] f($sum(b,2)): $int
[ OK ] term_indexing_one_side_interp_04_c
Running term_indexing_one_side_interp_04_d...
[ OK ] g(f($sum(b,2))): $int
[ OK ] term_indexing_one_side_interp_04_d
Running term_indexing_one_side_interp_05...
[ OK ] $sum(b,2): $int
[ OK ] term_indexing_one_side_interp_05
Running term_indexing_one_side_interp_06...
[ OK ] X0: $int
[ OK ] term_indexing_one_side_interp_06
Running term_indexing_one_side_interp_07...
[ OK ] f(a): $int
[ OK ] term_indexing_one_side_interp_07
Running term_indexing_one_side_interp_08...
[ OK ] $sum(3,a): $int
[ OK ] term_indexing_one_side_interp_08
Running term_indexing_poly_01...
[ OK ] h(X101): X101
[ OK ] h('A'): 'A'
[ OK ] term_indexing_poly_01
Running hol_0101...
[ OK ] f3(vAPP(sTfun(srt,srt),srt,h,f2),X1,X1): srt
[ OK ] hol_0101
Running hol_0102...
[ OK ] f3(X0,X0,vAPP(sTfun(srt,srt),srt,h,f1)): srt
[ OK ] hol_0102
Running hol_02...
[ OK ] f3(vAPP(sTfun(srt,srt),srt,h,f2),X1,X1): srt
[ OK ] hol_02
Running hol_03...
[ OK ] vAPP(sTfun(srt,srt),srt,h1,f2): srt
[ OK ] hol_03
Running hol_04_01...
[ OK ] vAPP(sTfun(srt,srt),srt,h(sTfun(srt,srt),srt),c1(sTfun(srt,srt))): srt
[ OK ] hol_04_01
Running hol_04_02...
[ OK ] vAPP(sTfun(srt,srt),srt,h(sTfun(srt,srt),srt),c2(sTfun(srt,srt))): srt
[ OK ] hol_04_02
Running hol_05_01...
[ OK ] vAPP(sTfun(srt,srt),srt,h(sTfun(srt,srt),srt),c1(sTfun(srt,srt))): srt
[ OK ] hol_05_01
Running hol_05_02...
[ OK ] vAPP(sTfun(srt,srt),srt,h(sTfun(srt,srt),srt),c2(sTfun(srt,srt))): srt
[ OK ] hol_05_02
Running hol_06...
[ OK ] vAPP($o,'A',f,a): 'A'
[ OK ] hol_06
Running term_indexing_poly_uwa_01...
[ OK ] f($int,$sum(a($int),X0)): $int
[ OK ] term_indexing_poly_uwa_01
Running term_indexing_interp_only...
[ OK ] $sum(b,2): $int
[ OK ] $sum(b,2): $int
[ OK ] term_indexing_interp_only
Running literal_indexing...
[ OK ] p($sum(b,2))
[ OK ] p($sum(b,2))
[ OK ] literal_indexing
Running higher_order...
[ OK ] vAPP(sTfun(srt,srt),srt,f,b): srt
[ OK ] X0: srt > srt
[ OK ] vAPP(sTfun(srt,srt),srt,f,b): srt
[ OK ] higher_order
Running higher_order2...
[ OK ] higher_order2
Running rob_unif_test_01...
[ OK ] f($sum(b,2)): $int unify f($sum(X0,2)): $int
[ OK ] rob_unif_test_01
Running rob_unif_test_02...
[ OK ] f($sum(b,2)): $int unify f($sum(X0,2)): $int
[ OK ] rob_unif_test_02
Running rob_unif_test_03...
[ OK ] f($sum(X0,2)): $int unify f(a): $int
[ OK ] rob_unif_test_03
Running rob_unif_test_04...
[ OK ] f(a): $int unify g($sum(1,a)): $int
[ OK ] rob_unif_test_04
Running rob_unif_test_05...
[ OK ] f($sum(a,b)): $int unify f($sum(X0,X1)): $int
[ OK ] rob_unif_test_05
Running rob_unif_test_06...
[ OK ] f2(X0,$sum(X0,1)): $int unify f2(a,a): $int
[ OK ] rob_unif_test_06
Running over_approx_test_2_bad_AC1...
[ OK ] f2(X0,$sum(a,X0)): $int unify f2(c,$sum(b,a)): $int
[ OK ] over_approx_test_2_bad_AC1
Running over_approx_test_2_bad_AC1_fixedPointIteration...
[ OK ] f2(X0,$sum(a,X0)): $int unify f2(c,$sum(b,a)): $int
[ OK ] over_approx_test_2_bad_AC1_fixedPointIteration
Running over_approx_test_2_good_AC1...
[ OK ] f2($sum(a,X0),X0): $int unify f2($sum(b,a),c): $int
[ OK ] over_approx_test_2_good_AC1
Running bottom_constraint_test_1_bad_AC1...
[ OK ] f2(f2(X1,X0),$sum($sum(a,X1),X0)): $int unify f2(f2(b,c),$sum($sum(c,b),a)): $int
[ OK ] bottom_constraint_test_1_bad_AC1
Running bottom_constraint_test_1_bad_AC1_fixedPointIteration...
[ OK ] f2(f2(X1,X0),$sum($sum(a,X1),X0)): $int unify f2(f2(b,c),$sum($sum(c,b),a)): $int
[ OK ] bottom_constraint_test_1_bad_AC1_fixedPointIteration
Running bottom_constraint_test_1_good_AC1...
[ OK ] f2($sum($sum(a,X0),X1),f2(X0,X1)): $int unify f2($sum($sum(c,b),a),f2(b,c)): $int
[ OK ] bottom_constraint_test_1_good_AC1
Running ac_bug_01...
[ OK ] $sum($sum($sum(a,b),c),a): $int unify $sum($sum($sum(a,b),X0),X1): $int
[ OK ] ac_bug_01
Running ac_test_01_AC1...
[ OK ] f2(b,$sum($sum(a,b),c)): $int unify f2(b,$sum($sum(X0,X1),c)): $int
[ OK ] ac_test_01_AC1
Running ac_test_02_AC1_good...
[ OK ] f2($sum($sum(a,b),c),c): $int unify f2($sum($sum(X0,X1),X2),X2): $int
[ OK ] ac_test_02_AC1_good
Running ac_test_02_AC1_bad...
[ OK ] f2(c,$sum($sum(a,b),c)): $int unify f2(X2,$sum($sum(X0,X1),X2)): $int
[ OK ] ac_test_02_AC1_bad
Running ac_test_02_AC1_bad_fixedPointIteration...
[ OK ] f2(c,$sum($sum(a,b),c)): $int unify f2(X2,$sum($sum(X0,X1),X2)): $int
[ OK ] ac_test_02_AC1_bad_fixedPointIteration
Running ac2_test_01...
[ OK ] f2(X0,$sum($sum(a,b),c)): $int unify f2(X0,$sum($sum(X0,b),a)): $int
[ OK ] ac2_test_01
Running ac2_test_02...
[ OK ] f2($sum($sum(a,b),c),f2(X0,b)): $int unify f2($sum($sum(X0,X1),a),f2(X0,X1)): $int
[ OK ] ac2_test_02
Running ac2_test_02_bad...
[ OK ] f2(f2(X0,b),$sum($sum(a,b),c)): $int unify f2(f2(X0,X1),$sum($sum(X0,X1),a)): $int
[ OK ] ac2_test_02_bad
Running ac2_test_02_bad_fixedPointIteration...
[ OK ] f2(f2(X0,b),$sum($sum(a,b),c)): $int unify f2(f2(X0,X1),$sum($sum(X0,X1),a)): $int
[ OK ] ac2_test_02_bad_fixedPointIteration
Running top_level_constraints_1...
[ OK ] $sum($sum(a,X1),X0): $int unify $sum($sum(a,b),c): $int
[ OK ] top_level_constraints_1
Running top_level_constraints_2_with_fixedPointIteration...
[ OK ] $sum($sum(a,X1),X0): $int
[ OK ] top_level_constraints_2_with_fixedPointIteration
Running top_level_constraints_2...
[ OK ] $sum($sum(a,X1),X0): $int
[ OK ] top_level_constraints_2
Running literal_tree_test_01...
[ OK ] $less(X0,$sum(1,$sum(X0,1)))
[ OK ] literal_tree_test_01
Running literal_tree_test_02...
[ OK ] $less(X0,$sum(1,$sum(X0,1)))
[ OK ] literal_tree_test_02
Tests run: 52
- ok 52 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 2.00 sec
----------------------------------------------------------
Test Passed.
"UnificationWithAbstraction" end time: Mar 19 03:04 CST
"UnificationWithAbstraction" time elapsed: 00:00:02
----------------------------------------------------------
4/38 Testing: GaussianElimination
4/38 Test: GaussianElimination
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "GaussianElimination"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"GaussianElimination" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running gve_test_1...
[ OK ] gve_test_1
Running gve_test_2...
[ OK ] gve_test_2
Running gve_test_3...
[ OK ] gve_test_3
Running gve_test_4...
[ OK ] gve_test_4
Running gve_test_uninterpreted...
[ OK ] gve_test_uninterpreted
Running gve_test_multiplesteps_1...
[ OK ] gve_test_multiplesteps_1
Running gve_test_multiplesteps_2...
[ OK ] gve_test_multiplesteps_2
Running gve_test_div...
[ OK ] gve_test_div
Running test_redundancy_01...
[ OK ] test_redundancy_01
Running test_redundancy_02...
[ OK ] test_redundancy_02
Running test_redundancy_03...
[ OK ] test_redundancy_03
Running test_redundancy_04...
[ OK ] test_redundancy_04
Running test_redundancy_05...
[ OK ] test_redundancy_05
Running test_redundancy_06...
[ OK ] test_redundancy_06
Tests run: 14
- ok 14 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.69 sec
----------------------------------------------------------
Test Passed.
"GaussianElimination" end time: Mar 19 03:04 CST
"GaussianElimination" time elapsed: 00:00:00
----------------------------------------------------------
5/38 Testing: PushUnaryMinus
5/38 Test: PushUnaryMinus
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "PushUnaryMinus"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"PushUnaryMinus" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running test_1...
[ OK ] test_1
Running test_2...
[ OK ] test_2
Running test_3...
[ OK ] test_3
Running test_4...
[ OK ] test_4
Running test_5...
[ OK ] test_5
Tests run: 5
- ok 5 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.21 sec
----------------------------------------------------------
Test Passed.
"PushUnaryMinus" end time: Mar 19 03:04 CST
"PushUnaryMinus" time elapsed: 00:00:00
----------------------------------------------------------
6/38 Testing: ArithmeticSubtermGeneralization
6/38 Test: ArithmeticSubtermGeneralization
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "ArithmeticSubtermGeneralization"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"ArithmeticSubtermGeneralization" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running single_var_01_Real...
[ OK ] single_var_01_Real
Running single_var_01_Rat...
[ OK ] single_var_01_Rat
Running single_var_01_Int...
[ OK ] single_var_01_Int
Running single_var_02_Real...
[ OK ] single_var_02_Real
Running single_var_02_Rat...
[ OK ] single_var_02_Rat
Running single_var_02_Int...
[ OK ] single_var_02_Int
Running single_var_03_Real...
[ OK ] single_var_03_Real
Running single_var_03_Rat...
[ OK ] single_var_03_Rat
Running single_var_03_Int...
[ OK ] single_var_03_Int
Running single_var_04_Real...
[ OK ] single_var_04_Real
Running single_var_04_Rat...
[ OK ] single_var_04_Rat
Running single_var_05_Real...
[ OK ] single_var_05_Real
Running single_var_05_Rat...
[ OK ] single_var_05_Rat
Running single_var_12_Real...
[ OK ] single_var_12_Real
Running single_var_12_Rat...
[ OK ] single_var_12_Rat
Running single_var_12_Int...
[ OK ] single_var_12_Int
Running single_var_18_Real...
[ OK ] single_var_18_Real
Running single_var_18_Rat...
[ OK ] single_var_18_Rat
Running single_var_power_01_Int...
[ OK ] single_var_power_01_Int
Running single_var_power_01_Rat...
[ OK ] single_var_power_01_Rat
Running single_var_power_01_Real...
[ OK ] single_var_power_01_Real
Running single_var_power_02_Int...
[ OK ] single_var_power_02_Int
Running single_var_power_02_Rat...
[ OK ] single_var_power_02_Rat
Running single_var_power_02_Real...
[ OK ] single_var_power_02_Real
Running multi_var_01_Real...
[ OK ] multi_var_01_Real
Running multi_var_01_Rat...
[ OK ] multi_var_01_Rat
Running multi_var_01_Int...
[ OK ] multi_var_01_Int
Running multi_var_02_Real...
[ OK ] multi_var_02_Real
Running multi_var_02_Rat...
[ OK ] multi_var_02_Rat
Running multi_var_02_Int...
[ OK ] multi_var_02_Int
Running multi_var_03_Real...
[ OK ] multi_var_03_Real
Running multi_var_03_Rat...
[ OK ] multi_var_03_Rat
Running multi_var_03_Int...
[ OK ] multi_var_03_Int
Running multi_var_04_Real...
[ OK ] multi_var_04_Real
Running multi_var_04_Rat...
[ OK ] multi_var_04_Rat
Running multi_var_04_Int...
[ OK ] multi_var_04_Int
Running multi_var_05_Real...
[ OK ] multi_var_05_Real
Running multi_var_05_Rat...
[ OK ] multi_var_05_Rat
Running multi_var_05_Int...
[ OK ] multi_var_05_Int
Running multi_var_06_Real...
[ OK ] multi_var_06_Real
Running multi_var_06_Rat...
[ OK ] multi_var_06_Rat
Running multi_var_06_Int...
[ OK ] multi_var_06_Int
Running multi_var_07_Real...
[ OK ] multi_var_07_Real
Running multi_var_07_Rat...
[ OK ] multi_var_07_Rat
Running multi_var_07_Int...
[ OK ] multi_var_07_Int
Running multi_var_08_Real...
[ OK ] multi_var_08_Real
Running multi_var_08_Rat...
[ OK ] multi_var_08_Rat
Running multi_var_09_Real...
[ OK ] multi_var_09_Real
Running multi_var_09_Rat...
[ OK ] multi_var_09_Rat
Running multi_var_10_Real...
[ OK ] multi_var_10_Real
Running multi_var_10_Rat...
[ OK ] multi_var_10_Rat
Running multi_var_11_Real...
[ OK ] multi_var_11_Real
Running multi_var_11_Rat...
[ OK ] multi_var_11_Rat
Running multi_var_12_Real...
[ OK ] multi_var_12_Real
Running multi_var_12_Rat...
[ OK ] multi_var_12_Rat
Running multi_var_13_Real...
[ OK ] multi_var_13_Real
Running multi_var_13_Rat...
[ OK ] multi_var_13_Rat
Running multi_var_14_Real...
[ OK ] multi_var_14_Real
Running multi_var_14_Rat...
[ OK ] multi_var_14_Rat
Running multi_var_15_Real...
[ OK ] multi_var_15_Real
Running multi_var_15_Rat...
[ OK ] multi_var_15_Rat
Running multi_var_16_Real...
[ OK ] multi_var_16_Real
Running multi_var_16_Rat...
[ OK ] multi_var_16_Rat
Running multi_var_18_Real...
[ OK ] multi_var_18_Real
Running multi_var_18_Rat...
[ OK ] multi_var_18_Rat
Running multi_var_19_Real...
[ OK ] multi_var_19_Real
Running multi_var_19_Rat...
[ OK ] multi_var_19_Rat
Running complex_expressions_01_Real...
[ OK ] complex_expressions_01_Real
Running complex_expressions_01_Rat...
[ OK ] complex_expressions_01_Rat
Running complex_expressions_01_Int...
[ OK ] complex_expressions_01_Int
Running complex_expressions_02_Real...
[ OK ] complex_expressions_02_Real
Running complex_expressions_02_Rat...
[ OK ] complex_expressions_02_Rat
Running fallancy_01_Real...
[ OK ] fallancy_01_Real
Running fallancy_01_Rat...
[ OK ] fallancy_01_Rat
Running fallancy_02_Real...
[ OK ] fallancy_02_Real
Running fallancy_02_Rat...
[ OK ] fallancy_02_Rat
Running fallancy_03_Real...
[ OK ] fallancy_03_Real
Running fallancy_03_Rat...
[ OK ] fallancy_03_Rat
Running fallancy_05_Real...
[ OK ] fallancy_05_Real
Running fallancy_05_Rat...
[ OK ] fallancy_05_Rat
Running fallancy_06_Real...
[ OK ] fallancy_06_Real
Running fallancy_06_Rat...
[ OK ] fallancy_06_Rat
Running fallancy_07_Real...
[ OK ] fallancy_07_Real
Running fallancy_07_Rat...
[ OK ] fallancy_07_Rat
Running fallancy_08_Real...
[ OK ] fallancy_08_Real
Running fallancy_08_Rat...
[ OK ] fallancy_08_Rat
Running generalize_var_1_Real...
[ OK ] generalize_var_1_Real
Running generalize_var_1_Rat...
[ OK ] generalize_var_1_Rat
Running generalize_var_1_Int...
[ OK ] generalize_var_1_Int
Running generalize_var_2_Real...
[ OK ] generalize_var_2_Real
Running generalize_var_2_Rat...
[ OK ] generalize_var_2_Rat
Running generalize_var_2_Int...
[ OK ] generalize_var_2_Int
Running generalize_var_3_Real...
[ OK ] generalize_var_3_Real
Running generalize_var_3_Rat...
[ OK ] generalize_var_3_Rat
Running generalize_var_3_Int...
[ OK ] generalize_var_3_Int
Running generalize_var_4_Real...
[ OK ] generalize_var_4_Real
Running generalize_var_4_Rat...
[ OK ] generalize_var_4_Rat
Running generalize_var_4_Int...
[ OK ] generalize_var_4_Int
Running generalize_var_5_Real...
[ OK ] generalize_var_5_Real
Running generalize_var_5_Rat...
[ OK ] generalize_var_5_Rat
Running generalize_var_5_Int...
[ OK ] generalize_var_5_Int
Running generalize_var_6_Real...
[ OK ] generalize_var_6_Real
Running generalize_var_6_Rat...
[ OK ] generalize_var_6_Rat
Running generalize_var_6_Int...
[ OK ] generalize_var_6_Int
Running generalize_var_7_Real...
[ OK ] generalize_var_7_Real
Running generalize_var_7_Rat...
[ OK ] generalize_var_7_Rat
Running generalize_var_7_Int...
[ OK ] generalize_var_7_Int
Running generalize_var_8_Real...
[ OK ] generalize_var_8_Real
Running generalize_var_8_Rat...
[ OK ] generalize_var_8_Rat
Running generalize_var_8_Int...
[ OK ] generalize_var_8_Int
Running generalize_var_9_Real...
[ OK ] generalize_var_9_Real
Running generalize_var_9_Rat...
[ OK ] generalize_var_9_Rat
Running generalize_var_9_Int...
[ OK ] generalize_var_9_Int
Running generalize_power_1_Real...
[ OK ] generalize_power_1_Real
Running generalize_power_2_Real...
[ OK ] generalize_power_2_Real
Running generalize_power_3_Real...
[ OK ] generalize_power_3_Real
Running generalize_power_4_Real...
[ OK ] generalize_power_4_Real
Running generalize_power_5_Real...
[ OK ] generalize_power_5_Real
Running bug_01_Real...
[ OK ] bug_01_Real
Running bug_02_Real...
[ OK ] bug_02_Real
Running bug_02_Rat...
[ OK ] bug_02_Rat
Running bug_02_Int...
[ OK ] bug_02_Int
Tests run: 122
- ok 122 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 5.87 sec
----------------------------------------------------------
Test Passed.
"ArithmeticSubtermGeneralization" end time: Mar 19 03:04 CST
"ArithmeticSubtermGeneralization" time elapsed: 00:00:05
----------------------------------------------------------
7/38 Testing: InterpretedFunctions
7/38 Test: InterpretedFunctions
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "InterpretedFunctions"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"InterpretedFunctions" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running partial_eval_add_1_Int...
[ OK ] partial_eval_add_1_Int
Running partial_eval_add_1_Rat...
[ OK ] partial_eval_add_1_Rat
Running partial_eval_add_1_Real...
[ OK ] partial_eval_add_1_Real
Running partial_eval_add_2_Int...
[ OK ] partial_eval_add_2_Int
Running partial_eval_add_2_Rat...
[ OK ] partial_eval_add_2_Rat
Running partial_eval_add_2_Real...
[ OK ] partial_eval_add_2_Real
Running partial_eval_add_3_Int...
[ OK ] partial_eval_add_3_Int
Running partial_eval_add_3_Rat...
[ OK ] partial_eval_add_3_Rat
Running partial_eval_add_3_Real...
[ OK ] partial_eval_add_3_Real
Running partial_eval_add_4_Int...
[ OK ] partial_eval_add_4_Int
Running partial_eval_add_4_Rat...
[ OK ] partial_eval_add_4_Rat
Running partial_eval_add_4_Real...
[ OK ] partial_eval_add_4_Real
Running simpl_times_zero_0_Int...
[ OK ] simpl_times_zero_0_Int
Running simpl_times_zero_0_Rat...
[ OK ] simpl_times_zero_0_Rat
Running simpl_times_zero_0_Real...
[ OK ] simpl_times_zero_0_Real
Running simpl_times_zero_1_Int...
[ OK ] simpl_times_zero_1_Int
Running simpl_times_zero_1_Rat...
[ OK ] simpl_times_zero_1_Rat
Running simpl_times_zero_1_Real...
[ OK ] simpl_times_zero_1_Real
Running simpl_times_zero_2_Int...
[ OK ] simpl_times_zero_2_Int
Running simpl_times_zero_2_Rat...
[ OK ] simpl_times_zero_2_Rat
Running simpl_times_zero_2_Real...
[ OK ] simpl_times_zero_2_Real
Running literal_to_const_0_Rat...
[ OK ] literal_to_const_0_Rat
Running literal_to_const_0_Real...
[ OK ] literal_to_const_0_Real
Running literal_to_const_1_Rat...
[ OK ] literal_to_const_1_Rat
Running literal_to_const_1_Real...
[ OK ] literal_to_const_1_Real
Running literal_to_const_2_Rat...
[ OK ] literal_to_const_2_Rat
Running literal_to_const_2_Real...
[ OK ] literal_to_const_2_Real
Running literal_to_const_3_Rat...
[ OK ] literal_to_const_3_Rat
Running literal_to_const_3_Real...
[ OK ] literal_to_const_3_Real
Running literal_to_const_4_Rat...
[ OK ] literal_to_const_4_Rat
Running literal_to_const_4_Real...
[ OK ] literal_to_const_4_Real
Running literal_to_const_5_Int...
[ OK ] literal_to_const_5_Int
Running literal_to_const_5_Rat...
[ OK ] literal_to_const_5_Rat
Running literal_to_const_5_Real...
[ OK ] literal_to_const_5_Real
Running literal_to_const_6_Int...
[ OK ] literal_to_const_6_Int
Running literal_to_const_6_Rat...
[ OK ] literal_to_const_6_Rat
Running literal_to_const_6_Real...
[ OK ] literal_to_const_6_Real
Running literal_to_const_7_Int...
[ OK ] literal_to_const_7_Int
Running literal_to_const_7_Rat...
[ OK ] literal_to_const_7_Rat
Running literal_to_const_7_Real...
[ OK ] literal_to_const_7_Real
Running literal_to_const_8_Int...
[ OK ] literal_to_const_8_Int
Running literal_to_const_8_Rat...
[ OK ] literal_to_const_8_Rat
Running literal_to_const_8_Real...
[ OK ] literal_to_const_8_Real
Running literal_to_const_9_Int...
[ OK ] literal_to_const_9_Int
Running literal_to_const_9_Rat...
[ OK ] literal_to_const_9_Rat
Running literal_to_const_9_Real...
[ OK ] literal_to_const_9_Real
Running literal_to_const_10_Int...
[ OK ] literal_to_const_10_Int
Running literal_to_const_10_Rat...
[ OK ] literal_to_const_10_Rat
Running literal_to_const_10_Real...
[ OK ] literal_to_const_10_Real
Running literal_to_const_11_Int...
[ OK ] literal_to_const_11_Int
Running literal_to_const_11_Rat...
[ OK ] literal_to_const_11_Rat
Running literal_to_const_11_Real...
[ OK ] literal_to_const_11_Real
Running eval_double_minus_1_1_Int...
[ OK ] eval_double_minus_1_1_Int
Running eval_double_minus_1_1_Rat...
[ OK ] eval_double_minus_1_1_Rat
Running eval_double_minus_1_1_Real...
[ OK ] eval_double_minus_1_1_Real
Running eval_double_minus_1_2_Int...
[ OK ] eval_double_minus_1_2_Int
Running eval_double_minus_1_2_Rat...
[ OK ] eval_double_minus_1_2_Rat
Running eval_double_minus_1_2_Real...
[ OK ] eval_double_minus_1_2_Real
Running eval_double_minus_2_1_Int...
[ OK ] eval_double_minus_2_1_Int
Running eval_double_minus_2_1_Rat...
[ OK ] eval_double_minus_2_1_Rat
Running eval_double_minus_2_1_Real...
[ OK ] eval_double_minus_2_1_Real
Running eval_double_minus_2_2_Int...
[ OK ] eval_double_minus_2_2_Int
Running eval_double_minus_2_2_Rat...
[ OK ] eval_double_minus_2_2_Rat
Running eval_double_minus_2_2_Real...
[ OK ] eval_double_minus_2_2_Real
Running eval_inverse_1_Int...
[ OK ] eval_inverse_1_Int
Running eval_inverse_1_Rat...
[ OK ] eval_inverse_1_Rat
Running eval_inverse_1_Real...
[ OK ] eval_inverse_1_Real
Running eval_double_minus_3_Int...
[ OK ] eval_double_minus_3_Int
Running eval_double_minus_3_Rat...
[ OK ] eval_double_minus_3_Rat
Running eval_double_minus_3_Real...
[ OK ] eval_double_minus_3_Real
Running eval_double_minus_4_Int...
[ OK ] eval_double_minus_4_Int
Running eval_double_minus_4_Rat...
[ OK ] eval_double_minus_4_Rat
Running eval_double_minus_4_Real...
[ OK ] eval_double_minus_4_Real
Running eval_remove_identity_1_Int...
[ OK ] eval_remove_identity_1_Int
Running eval_remove_identity_1_Rat...
[ OK ] eval_remove_identity_1_Rat
Running eval_remove_identity_1_Real...
[ OK ] eval_remove_identity_1_Real
Running eval_remove_identity_2_Int...
[ OK ] eval_remove_identity_2_Int
Running eval_remove_identity_2_Rat...
[ OK ] eval_remove_identity_2_Rat
Running eval_remove_identity_2_Real...
[ OK ] eval_remove_identity_2_Real
Running polynomial__normalize_uminus_1_Int...
[ OK ] polynomial__normalize_uminus_1_Int
Running polynomial__normalize_uminus_1_Rat...
[ OK ] polynomial__normalize_uminus_1_Rat
Running polynomial__normalize_uminus_1_Real...
[ OK ] polynomial__normalize_uminus_1_Real
Running polynomial__normalize_uminus_2_Int...
[ OK ] polynomial__normalize_uminus_2_Int
Running polynomial__normalize_uminus_2_Rat...
[ OK ] polynomial__normalize_uminus_2_Rat
Running polynomial__normalize_uminus_2_Real...
[ OK ] polynomial__normalize_uminus_2_Real
Running polynomial__normalize_uminus_3_Int...
[ OK ] polynomial__normalize_uminus_3_Int
Running polynomial__normalize_uminus_3_Rat...
[ OK ] polynomial__normalize_uminus_3_Rat
Running polynomial__normalize_uminus_3_Real...
[ OK ] polynomial__normalize_uminus_3_Real
Running polynomial__merge_consts_1_Int...
[ OK ] polynomial__merge_consts_1_Int
Running polynomial__merge_consts_1_Rat...
[ OK ] polynomial__merge_consts_1_Rat
Running polynomial__merge_consts_1_Real...
[ OK ] polynomial__merge_consts_1_Real
Running polynomial__merge_consts_2_Int...
[ OK ] polynomial__merge_consts_2_Int
Running polynomial__merge_consts_2_Rat...
[ OK ] polynomial__merge_consts_2_Rat
Running polynomial__merge_consts_2_Real...
[ OK ] polynomial__merge_consts_2_Real
Running polynomial__merge_consts_3_Int...
[ OK ] polynomial__merge_consts_3_Int
Running polynomial__merge_consts_3_Rat...
[ OK ] polynomial__merge_consts_3_Rat
Running polynomial__merge_consts_3_Real...
[ OK ] polynomial__merge_consts_3_Real
Running polynomial__push_unary_minus_Int...
[ OK ] polynomial__push_unary_minus_Int
Running polynomial__push_unary_minus_Rat...
[ OK ] polynomial__push_unary_minus_Rat
Running polynomial__push_unary_minus_Real...
[ OK ] polynomial__push_unary_minus_Real
Running test_div_1_Rat...
[ OK ] test_div_1_Rat
Running test_div_1_Real...
[ OK ] test_div_1_Real
Running eval_test_cached_1_Int...
[ OK ] eval_test_cached_1_Int
Running eval_test_cached_1_Rat...
[ OK ] eval_test_cached_1_Rat
Running eval_test_cached_1_Real...
[ OK ] eval_test_cached_1_Real
Running eval_test_cached_2_Int...
[ OK ] eval_test_cached_2_Int
Running eval_test_cached_2_Rat...
[ OK ] eval_test_cached_2_Rat
Running eval_test_cached_2_Real...
[ OK ] eval_test_cached_2_Real
Running eval_bug_1_Int...
[ OK ] eval_bug_1_Int
Running eval_bug_1_Rat...
[ OK ] eval_bug_1_Rat
Running eval_bug_1_Real...
[ OK ] eval_bug_1_Real
Running eval_bug_2_Int...
[ OK ] eval_bug_2_Int
Running eval_bug_2_Rat...
[ OK ] eval_bug_2_Rat
Running eval_bug_2_Real...
[ OK ] eval_bug_2_Real
Running eval_bug_3_Int...
[ OK ] eval_bug_3_Int
Running eval_bug_3_Rat...
[ OK ] eval_bug_3_Rat
Running eval_bug_3_Real...
[ OK ] eval_bug_3_Real
Running eval_bug_4_Int...
[ OK ] eval_bug_4_Int
Running eval_bug_4_Rat...
[ OK ] eval_bug_4_Rat
Running eval_bug_4_Real...
[ OK ] eval_bug_4_Real
Running eval_bug_5_Int...
[ OK ] eval_bug_5_Int
Running eval_bug_5_Rat...
[ OK ] eval_bug_5_Rat
Running eval_bug_5_Real...
[ OK ] eval_bug_5_Real
Running eval_bug_7_Int...
[ OK ] eval_bug_7_Int
Running eval_bug_7_Rat...
[ OK ] eval_bug_7_Rat
Running eval_bug_7_Real...
[ OK ] eval_bug_7_Real
Running eval_cancellation_add_0_Int...
[ OK ] eval_cancellation_add_0_Int
Running eval_cancellation_add_0_Rat...
[ OK ] eval_cancellation_add_0_Rat
Running eval_cancellation_add_0_Real...
[ OK ] eval_cancellation_add_0_Real
Running eval_cancellation_add_1_Int...
[ OK ] eval_cancellation_add_1_Int
Running eval_cancellation_add_1_Rat...
[ OK ] eval_cancellation_add_1_Rat
Running eval_cancellation_add_1_Real...
[ OK ] eval_cancellation_add_1_Real
Running eval_cancellation_add_2_Int...
[ OK ] eval_cancellation_add_2_Int
Running eval_cancellation_add_2_Rat...
[ OK ] eval_cancellation_add_2_Rat
Running eval_cancellation_add_2_Real...
[ OK ] eval_cancellation_add_2_Real
Running eval_cancellation_add_3_Int...
[ OK ] eval_cancellation_add_3_Int
Running eval_cancellation_add_3_Rat...
[ OK ] eval_cancellation_add_3_Rat
Running eval_cancellation_add_3_Real...
[ OK ] eval_cancellation_add_3_Real
Running eval_cancellation_add_4_Int...
[ OK ] eval_cancellation_add_4_Int
Running eval_cancellation_add_4_Rat...
[ OK ] eval_cancellation_add_4_Rat
Running eval_cancellation_add_4_Real...
[ OK ] eval_cancellation_add_4_Real
Running eval_cancellation_add_5_Int...
[ OK ] eval_cancellation_add_5_Int
Running eval_cancellation_add_5_Rat...
[ OK ] eval_cancellation_add_5_Rat
Running eval_cancellation_add_5_Real...
[ OK ] eval_cancellation_add_5_Real
Running eval_cancellation_add_6_Int...
[ OK ] eval_cancellation_add_6_Int
Running eval_cancellation_add_6_Rat...
[ OK ] eval_cancellation_add_6_Rat
Running eval_cancellation_add_6_Real...
[ OK ] eval_cancellation_add_6_Real
Running eval_cancellation_add_8_Int...
[ OK ] eval_cancellation_add_8_Int
Running eval_cancellation_add_8_Rat...
[ OK ] eval_cancellation_add_8_Rat
Running eval_cancellation_add_8_Real...
[ OK ] eval_cancellation_add_8_Real
Running eval_cancellation_add_9_Int...
[ OK ] eval_cancellation_add_9_Int
Running eval_cancellation_add_9_Rat...
[ OK ] eval_cancellation_add_9_Rat
Running eval_cancellation_add_9_Real...
[ OK ] eval_cancellation_add_9_Real
Running eval_cancellation_add_10_Int...
[ OK ] eval_cancellation_add_10_Int
Running eval_cancellation_add_10_Rat...
[ OK ] eval_cancellation_add_10_Rat
Running eval_cancellation_add_10_Real...
[ OK ] eval_cancellation_add_10_Real
Running eval_cancellation_add_11_Int...
[ OK ] eval_cancellation_add_11_Int
Running eval_cancellation_add_11_Rat...
[ OK ] eval_cancellation_add_11_Rat
Running eval_cancellation_add_11_Real...
[ OK ] eval_cancellation_add_11_Real
Running eval_quotientE_1_Int...
[ OK ] eval_quotientE_1_Int
Running eval_quotientE_2_Int...
[ OK ] eval_quotientE_2_Int
Running eval_quotientE_3_Int...
[ OK ] eval_quotientE_3_Int
Running eval_quotientE_4_Int...
[ OK ] eval_quotientE_4_Int
Running eval_quotientE_4_1_Int...
[ OK ] eval_quotientE_4_1_Int
Running eval_quotientF_1_Int...
[ OK ] eval_quotientF_1_Int
Running eval_quotientT_1_Int...
[ OK ] eval_quotientT_1_Int
Running eval_quotient_1_Rat...
[ OK ] eval_quotient_1_Rat
Running eval_quotient_1_Real...
[ OK ] eval_quotient_1_Real
Running div_zero_0_Rat...
[ OK ] div_zero_0_Rat
Running div_zero_0_Real...
[ OK ] div_zero_0_Real
Running div_zero_1_Int...
[ OK ] div_zero_1_Int
Running div_zero_2_Int...
[ OK ] div_zero_2_Int
Running eval_overflow_1_Int...
[ OK ] eval_overflow_1_Int
Running eval_overflow_1_Rat...
[ OK ] eval_overflow_1_Rat
Running eval_overflow_1_Real...
[ OK ] eval_overflow_1_Real
Running eval_overflow_2_Int...
[ OK ] eval_overflow_2_Int
Running eval_overflow_2_Rat...
[ OK ] eval_overflow_2_Rat
Running eval_overflow_2_Real...
[ OK ] eval_overflow_2_Real
Running eval_overflow_3_Int...
[ OK ] eval_overflow_3_Int
Running eval_overflow_3_Rat...
[ OK ] eval_overflow_3_Rat
Running eval_overflow_3_Real...
[ OK ] eval_overflow_3_Real
Running eval_overflow_4_Int...
[ OK ] eval_overflow_4_Int
Running eval_overflow_4_Rat...
[ OK ] eval_overflow_4_Rat
Running eval_overflow_4_Real...
[ OK ] eval_overflow_4_Real
Running eval_overflow_5_Int...
[ OK ] eval_overflow_5_Int
Running eval_overflow_5_Rat...
[ OK ] eval_overflow_5_Rat
Running eval_overflow_5_Real...
[ OK ] eval_overflow_5_Real
Running eval_overflow_6_Rat...
[ OK ] eval_overflow_6_Rat
Running eval_overflow_6_Real...
[ OK ] eval_overflow_6_Real
Running eval_overflow_7_Rat...
[ OK ] eval_overflow_7_Rat
Running eval_overflow_7_Real...
[ OK ] eval_overflow_7_Real
Running NUM_IS_NUM_01_Int...
[ OK ] NUM_IS_NUM_01_Int
Running NUM_IS_NUM_01_Rat...
[ OK ] NUM_IS_NUM_01_Rat
Running NUM_IS_NUM_01_Real...
[ OK ] NUM_IS_NUM_01_Real
Running NUM_IS_NUM_02_Int...
[ OK ] NUM_IS_NUM_02_Int
Running NUM_IS_NUM_02_Rat...
[ OK ] NUM_IS_NUM_02_Rat
Running NUM_IS_NUM_02_Real...
[ OK ] NUM_IS_NUM_02_Real
Running NUM_IS_NUM_03_Rat...
[ OK ] NUM_IS_NUM_03_Rat
Running NUM_IS_NUM_03_Real...
[ OK ] NUM_IS_NUM_03_Real
Running NUM_IS_NUM_04_Rat...
[ OK ] NUM_IS_NUM_04_Rat
Running NUM_IS_NUM_04_Real...
[ OK ] NUM_IS_NUM_04_Real
Running NUM_IS_NUM_05_Rat...
[ OK ] NUM_IS_NUM_05_Rat
Running NUM_IS_NUM_05_Real...
[ OK ] NUM_IS_NUM_05_Real
Running NUM_IS_NUM_06_Rat...
[ OK ] NUM_IS_NUM_06_Rat
Running NUM_IS_NUM_06_Real...
[ OK ] NUM_IS_NUM_06_Real
Running NUM_IS_NUM_07_Rat...
[ OK ] NUM_IS_NUM_07_Rat
Running NUM_IS_NUM_07_Real...
[ OK ] NUM_IS_NUM_07_Real
Running NUM_IS_NUM_08_Int...
[ OK ] NUM_IS_NUM_08_Int
Running NUM_IS_NUM_08_Rat...
[ OK ] NUM_IS_NUM_08_Rat
Running NUM_IS_NUM_08_Real...
[ OK ] NUM_IS_NUM_08_Real
Tests run: 210
- ok 210 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 9.83 sec
----------------------------------------------------------
Test Passed.
"InterpretedFunctions" end time: Mar 19 03:04 CST
"InterpretedFunctions" time elapsed: 00:00:09
----------------------------------------------------------
8/38 Testing: Rebalance
8/38 Test: Rebalance
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Rebalance"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Rebalance" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running constants_1_Real...
[ OK ] constants_1_Real
Running constants_1_Rat...
[ OK ] constants_1_Rat
Running constants_1_Int...
[ OK ] constants_1_Int
Running constants_2_Real...
[ OK ] constants_2_Real
Running constants_2_Rat...
[ OK ] constants_2_Rat
Running constants_2_Int...
[ OK ] constants_2_Int
Running uninterpreted_1_Real...
[ OK ] uninterpreted_1_Real
Running uninterpreted_1_Rat...
[ OK ] uninterpreted_1_Rat
Running uninterpreted_1_Int...
[ OK ] uninterpreted_1_Int
Running uninterpreted_2_Real...
[ OK ] uninterpreted_2_Real
Running uninterpreted_2_Rat...
[ OK ] uninterpreted_2_Rat
Running uninterpreted_2_Int...
[ OK ] uninterpreted_2_Int
Running multi_var_1_Real...
[ OK ] multi_var_1_Real
Running multi_var_1_Rat...
[ OK ] multi_var_1_Rat
Running multi_var_1_Int...
[ OK ] multi_var_1_Int
Running multi_var_2_Real...
[ OK ] multi_var_2_Real
Running multi_var_2_Rat...
[ OK ] multi_var_2_Rat
Running multi_var_2_Int...
[ OK ] multi_var_2_Int
Running multi_var_3_Real...
[ OK ] multi_var_3_Real
Running multi_var_3_Rat...
[ OK ] multi_var_3_Rat
Running multi_var_3_Int...
[ OK ] multi_var_3_Int
Running multi_var_4_Real...
[ OK ] multi_var_4_Real
Running multi_var_4_Rat...
[ OK ] multi_var_4_Rat
Running multi_var_4_Int...
[ OK ] multi_var_4_Int
Running multi_var_5_Real...
[ OK ] multi_var_5_Real
Running multi_var_5_Rat...
[ OK ] multi_var_5_Rat
Running multi_var_5_Int...
[ OK ] multi_var_5_Int
Running rebalance_multiple_vars_Real...
[ OK ] rebalance_multiple_vars_Real
Running rebalance_multiple_vars_Rat...
[ OK ] rebalance_multiple_vars_Rat
Running rebalance_multiple_vars_Int...
[ OK ] rebalance_multiple_vars_Int
Running div_zero_1_Real...
[ OK ] div_zero_1_Real
Running div_zero_1_Rat...
[ OK ] div_zero_1_Rat
Running div_zero_1_Int...
[ OK ] div_zero_1_Int
Running div_zero_2_Real...
[ OK ] div_zero_2_Real
Running div_zero_2_Rat...
[ OK ] div_zero_2_Rat
Running div_zero_2_Int...
[ OK ] div_zero_2_Int
Running div_zero_3_Real...
[ OK ] div_zero_3_Real
Running div_zero_3_Rat...
[ OK ] div_zero_3_Rat
Running div_zero_3_Int...
[ OK ] div_zero_3_Int
Running div_zero_4_Real...
[ OK ] div_zero_4_Real
Running div_zero_4_Rat...
[ OK ] div_zero_4_Rat
Running div_zero_4_Int...
[ OK ] div_zero_4_Int
Running div_zero_5_Real...
[ OK ] div_zero_5_Real
Running div_zero_5_Rat...
[ OK ] div_zero_5_Rat
Running div_zero_5_Int...
[ OK ] div_zero_5_Int
Running div_zero_6_Real...
[ OK ] div_zero_6_Real
Running div_zero_6_Rat...
[ OK ] div_zero_6_Rat
Running div_zero_6_Int...
[ OK ] div_zero_6_Int
Running bug_1_Real...
[ OK ] bug_1_Real
Running bug_1_Rat...
[ OK ] bug_1_Rat
Running bug_1_Int...
[ OK ] bug_1_Int
Running bug_2_Real...
[ OK ] bug_2_Real
Running bug_2_Rat...
[ OK ] bug_2_Rat
Running bug_2_Int...
[ OK ] bug_2_Int
Tests run: 54
- ok 54 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 1.61 sec
----------------------------------------------------------
Test Passed.
"Rebalance" end time: Mar 19 03:04 CST
"Rebalance" time elapsed: 00:00:01
----------------------------------------------------------
9/38 Testing: Disagreement
9/38 Test: Disagreement
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Disagreement"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Disagreement" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running dis1...
[ OK ] dis1
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.12 sec
----------------------------------------------------------
Test Passed.
"Disagreement" end time: Mar 19 03:04 CST
"Disagreement" time elapsed: 00:00:00
----------------------------------------------------------
10/38 Testing: DynamicHeap
10/38 Test: DynamicHeap
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "DynamicHeap"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"DynamicHeap" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running dheapFewElements...
[ OK ] dheapFewElements
Running dheapMoreElements...
[ OK ] dheapMoreElements
Running dheapDecreasing...
[ OK ] dheapDecreasing
Running dheapIncreasing...
[ OK ] dheapIncreasing
Tests run: 4
- ok 4 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.18 sec
----------------------------------------------------------
Test Passed.
"DynamicHeap" end time: Mar 19 03:04 CST
"DynamicHeap" time elapsed: 00:00:00
----------------------------------------------------------
11/38 Testing: Induction
11/38 Test: Induction
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Induction"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Induction" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running test_tester1...
[ OK ] test_tester1
Running test_tester2...
[ OK ] test_tester2
Running test_tester3...
[ OK ] test_tester3
Running test_tester4...
[ OK ] test_tester4
Running test_01...
[ OK ] test_01
Running test_02...
[ OK ] test_02
Running test_03...
[ OK ] test_03
Running test_04...
[ OK ] test_04
Running test_05...
[ OK ] test_05
Running test_07...
[ OK ] test_07
Running test_08...
[ OK ] test_08
Running test_09...
[ OK ] test_09
Running test_10...
[ OK ] test_10
Running test_11...
[ OK ] test_11
Running test_12...
[ OK ] test_12
Running test_13...
[ OK ] test_13
Running test_14...
[ OK ] test_14
Running test_15...
[ OK ] test_15
Running test_16...
[ OK ] test_16
Running test_17...
[ OK ] test_17
Running test_18...
[ OK ] test_18
Running test_19...
[ OK ] test_19
Running test_20...
[ OK ] test_20
Running test_21...
[ OK ] test_21
Running test_22...
[ OK ] test_22
Running test_23...
[ OK ] test_23
Running test_24...
[ OK ] test_24
Running test_25...
[ OK ] test_25
Running test_26...
[ OK ] test_26
Running test_27...
[ OK ] test_27
Running test_28...
[ OK ] test_28
Running test_29...
[ OK ] test_29
Running test_30...
[ OK ] test_30
Running test_31...
[ OK ] test_31
Running test_32...
[ OK ] test_32
Running test_33...
[ OK ] test_33
Running test_34...
[ OK ] test_34
Running test_35...
[ OK ] test_35
Running test_36...
[ OK ] test_36
Running test_37...
[ OK ] test_37
Running generalizations_01...
[ OK ] generalizations_01
Running generalizations_02...
[ OK ] generalizations_02
Running generalizations_03...
[ OK ] generalizations_03
Tests run: 43
- ok 43 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 4.14 sec
----------------------------------------------------------
Test Passed.
"Induction" end time: Mar 19 03:04 CST
"Induction" time elapsed: 00:00:04
----------------------------------------------------------
12/38 Testing: IntegerConstantType
12/38 Test: IntegerConstantType
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "IntegerConstantType"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"IntegerConstantType" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running list_1...
[ OK ] list_1
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.10 sec
----------------------------------------------------------
Test Passed.
"IntegerConstantType" end time: Mar 19 03:04 CST
"IntegerConstantType" time elapsed: 00:00:00
----------------------------------------------------------
13/38 Testing: SATSolver
13/38 Test: SATSolver
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "SATSolver"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"SATSolver" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running testProofWithAssums...
[ OK ] testProofWithAssums
Running testSATSolverInterface...
Minisat
Random: 0011001011 Fixed: 1111111111
[ OK ] testSATSolverInterface
Running testSolvingUnderAssumptions...
Minisat
bed
bed
[ OK ] testSolvingUnderAssumptions
Tests run: 3
- ok 3 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.14 sec
----------------------------------------------------------
Test Passed.
"SATSolver" end time: Mar 19 03:04 CST
"SATSolver" time elapsed: 00:00:00
----------------------------------------------------------
14/38 Testing: ArithCompare
14/38 Test: ArithCompare
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "ArithCompare"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"ArithCompare" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running testArithCompareSAT...
[ OK ] testArithCompareSAT
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.10 sec
----------------------------------------------------------
Test Passed.
"ArithCompare" end time: Mar 19 03:04 CST
"ArithCompare" time elapsed: 00:00:00
----------------------------------------------------------
15/38 Testing: SyntaxSugar
15/38 Test: SyntaxSugar
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "SyntaxSugar"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"SyntaxSugar" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running some_meaningful_testname...
[ OK ] some_meaningful_testname
Running some_other_meaningful_testname...
[ OK ] some_other_meaningful_testname
Running uninterpreted_and_interpreted_stuff...
[ OK ] uninterpreted_and_interpreted_stuff
Running only_uninterpreted_stuff...
[ OK ] only_uninterpreted_stuff
Running watch_out_for_this...
[ OK ] watch_out_for_this
Running get_functors...
[ OK ] get_functors
Running create_equalities...
[ OK ] create_equalities
Running term_algebra...
[ OK ] term_algebra
Tests run: 8
- ok 8 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.27 sec
----------------------------------------------------------
Test Passed.
"SyntaxSugar" end time: Mar 19 03:04 CST
"SyntaxSugar" time elapsed: 00:00:00
----------------------------------------------------------
16/38 Testing: SkipList
16/38 Test: SkipList
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "SkipList"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"SkipList" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running skiplist1...
[ OK ] skiplist1
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 1.11 sec
----------------------------------------------------------
Test Passed.
"SkipList" end time: Mar 19 03:04 CST
"SkipList" time elapsed: 00:00:01
----------------------------------------------------------
17/38 Testing: BinaryHeap
17/38 Test: BinaryHeap
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "BinaryHeap"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"BinaryHeap" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running bheap1...
[ OK ] bheap1
Running bheap2...
[ OK ] bheap2
Tests run: 2
- ok 2 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.12 sec
----------------------------------------------------------
Test Passed.
"BinaryHeap" end time: Mar 19 03:04 CST
"BinaryHeap" time elapsed: 00:00:00
----------------------------------------------------------
18/38 Testing: SafeRecursion
18/38 Test: SafeRecursion
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "SafeRecursion"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"SafeRecursion" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running safeRecMaxDeg...
[ OK ] safeRecMaxDeg
Running safeRecStrRep...
[ OK ] safeRecStrRep
Tests run: 2
- ok 2 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.12 sec
----------------------------------------------------------
Test Passed.
"SafeRecursion" end time: Mar 19 03:04 CST
"SafeRecursion" time elapsed: 00:00:00
----------------------------------------------------------
19/38 Testing: KBO
19/38 Test: KBO
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "KBO"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"KBO" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running kbo_test01...
[ OK ] kbo_test01
Running kbo_test02...
[ OK ] kbo_test02
Running kbo_test03...
[ OK ] kbo_test03
Running kbo_test04...
[ OK ] kbo_test04
Running kbo_test05...
[ OK ] kbo_test05
Running kbo_test06...
[ OK ] kbo_test06
Running kbo_test07...
[ OK ] kbo_test07
Running kbo_test08...
[ OK ] kbo_test08
Running kbo_test09...
[ OK ] kbo_test09
Running kbo_test10...
[ OK ] kbo_test10
Running kbo_test11...
[ OK ] kbo_test11
Running kbo_test12...
[ OK ] kbo_test12
Running kbo_test13...
[ OK ] kbo_test13
Running kbo_test14...
[ OK ] kbo_test14
Running kbo_test15...
[ OK ] kbo_test15
Running kbo_test16...
[ OK ] kbo_test16
Running kbo_test17...
[ OK ] kbo_test17
Running kbo_test18...
[ OK ] kbo_test18
Running kbo_test19...
[ OK ] kbo_test19
Running kbo_test20...
[ OK ] kbo_test20
Running kbo_test21...
[ OK ] kbo_test21
Running kbo_test22...
[ OK ] kbo_test22
Running kbo_test23...
[ OK ] kbo_test23
Tests run: 23
- ok 23 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.86 sec
----------------------------------------------------------
Test Passed.
"KBO" end time: Mar 19 03:04 CST
"KBO" time elapsed: 00:00:00
----------------------------------------------------------
20/38 Testing: SKIKBO
20/38 Test: SKIKBO
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "SKIKBO"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"SKIKBO" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running skikbo_test01...
[ OK ] skikbo_test01
Running skikbo_test02...
[ OK ] skikbo_test02
Running skikbo_test03...
[ OK ] skikbo_test03
Running skikbo_test04...
[ OK ] skikbo_test04
Running skikbo_test05...
[ OK ] skikbo_test05
Running skikbo_test06...
[ OK ] skikbo_test06
Tests run: 6
- ok 6 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.23 sec
----------------------------------------------------------
Test Passed.
"SKIKBO" end time: Mar 19 03:04 CST
"SKIKBO" time elapsed: 00:00:00
----------------------------------------------------------
21/38 Testing: LPO
21/38 Test: LPO
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "LPO"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"LPO" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running lpo_test01...
[ OK ] lpo_test01
Running lpo_test02...
[ OK ] lpo_test02
Running lpo_test03...
[ OK ] lpo_test03
Running lpo_test04...
[ OK ] lpo_test04
Running lpo_test05...
[ OK ] lpo_test05
Tests run: 5
- ok 5 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.19 sec
----------------------------------------------------------
Test Passed.
"LPO" end time: Mar 19 03:04 CST
"LPO" time elapsed: 00:00:00
----------------------------------------------------------
22/38 Testing: RatioKeeper
22/38 Test: RatioKeeper
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "RatioKeeper"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"RatioKeeper" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running rkeeper1...
[ OK ] rkeeper1
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.10 sec
----------------------------------------------------------
Test Passed.
"RatioKeeper" end time: Mar 19 03:04 CST
"RatioKeeper" time elapsed: 00:00:00
----------------------------------------------------------
23/38 Testing: OptionConstraints
23/38 Test: OptionConstraints
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "OptionConstraints"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"OptionConstraints" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running int_bounds...
User error:
Broken Constraint: naming(327681) is less than 32768
WARNING Broken Constraint: lrs_first_time_check(200) is less than 100
WARNING Broken Constraint: lrs_first_time_check(-200) is greater than or equal to 0
WARNING Broken Constraint: if extensionality_max_length(1) has been set then extensionality_resolution(off) is not equal to off
[ OK ] int_bounds
Running default_dependence...
WARNING Broken Constraint: if extensionality_allow_pos_eq(on) has been set then extensionality_resolution(off) is equal to filter
[ OK ] default_dependence
Tests run: 2
- ok 2 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.27 sec
----------------------------------------------------------
Test Passed.
"OptionConstraints" end time: Mar 19 03:04 CST
"OptionConstraints" time elapsed: 00:00:00
----------------------------------------------------------
24/38 Testing: DHMultiset
24/38 Test: DHMultiset
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "DHMultiset"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"DHMultiset" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running dhmultiset1...
[ OK ] dhmultiset1
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.21 sec
----------------------------------------------------------
Test Passed.
"DHMultiset" end time: Mar 19 03:04 CST
"DHMultiset" time elapsed: 00:00:00
----------------------------------------------------------
25/38 Testing: List
25/38 Test: List
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "List"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"List" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running list1...
[ OK ] list1
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.10 sec
----------------------------------------------------------
Test Passed.
"List" end time: Mar 19 03:04 CST
"List" time elapsed: 00:00:00
----------------------------------------------------------
26/38 Testing: BottomUpEvaluation
26/38 Test: BottomUpEvaluation
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "BottomUpEvaluation"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"BottomUpEvaluation" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running example_01__replace_all_vars_by_term...
[ OK ] example_01__replace_all_vars_by_term
Running example_02__compute_size...
[ OK ] example_02__compute_size
Tests run: 2
- ok 2 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.14 sec
----------------------------------------------------------
Test Passed.
"BottomUpEvaluation" end time: Mar 19 03:04 CST
"BottomUpEvaluation" time elapsed: 00:00:00
----------------------------------------------------------
27/38 Testing: Coproduct
27/38 Test: Coproduct
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Coproduct"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Coproduct" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running examples__is_variant_01...
[ OK ] examples__is_variant_01
Running examples__is_variant_02...
[ OK ] examples__is_variant_02
Running examples__is_variant_03...
[ OK ] examples__is_variant_03
Running examples__equal_01...
[ OK ] examples__equal_01
Running examples__equal_02...
[ OK ] examples__equal_02
Running examples__equal_03...
[ OK ] examples__equal_03
Running examples__match_01...
[ OK ] examples__match_01
Running examples__match_02...
[ OK ] examples__match_02
Running examples__compare...
[ OK ] examples__compare
Running unwrap_01...
[ OK ] unwrap_01
Running unwrap_02...
[ OK ] unwrap_02
Running move_01...
[ OK ] move_01
Running apply01...
[ OK ] apply01
Tests run: 13
- ok 13 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.31 sec
----------------------------------------------------------
Test Passed.
"Coproduct" end time: Mar 19 03:04 CST
"Coproduct" time elapsed: 00:00:00
----------------------------------------------------------
28/38 Testing: EqualityResolution
28/38 Test: EqualityResolution
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "EqualityResolution"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"EqualityResolution" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running test_01...
[ OK ] test_01
Running test_02...
[ OK ] test_02
Running test_03...
[ OK ] test_03
Running test_04...
[ OK ] test_04
Running test_05...
[ OK ] test_05
Running test_06...
[ OK ] test_06
Tests run: 6
- ok 6 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.36 sec
----------------------------------------------------------
Test Passed.
"EqualityResolution" end time: Mar 19 03:04 CST
"EqualityResolution" time elapsed: 00:00:00
----------------------------------------------------------
29/38 Testing: Iterator
29/38 Test: Iterator
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Iterator"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Iterator" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running test_collect...
[ OK ] test_collect
Running test_map...
[ OK ] test_map
Running test_filter...
[ OK ] test_filter
Running test_foreach...
[ OK ] test_foreach
Running test_for...
[ OK ] test_for
Running testFlatMap1...
[ OK ] testFlatMap1
Running testFlatMap2...
[ OK ] testFlatMap2
Tests run: 7
- ok 7 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.20 sec
----------------------------------------------------------
Test Passed.
"Iterator" end time: Mar 19 03:04 CST
"Iterator" time elapsed: 00:00:00
----------------------------------------------------------
30/38 Testing: Option
30/38 Test: Option
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Option"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Option" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running examples__isNone...
[ OK ] examples__isNone
Running examples__isSome...
[ OK ] examples__isSome
Running examples__match...
[ OK ] examples__match
Running examples__unwrapOrElse...
[ OK ] examples__unwrapOrElse
Running examples__unwrapOrInit...
[ OK ] examples__unwrapOrInit
Running examples__toOwned...
[ OK ] examples__toOwned
Running examples__map...
[ OK ] examples__map
Running examples__andThen...
[ OK ] examples__andThen
Running test_LeaqueChecker_1...
[ OK ] test_LeaqueChecker_1
Running test_LeaqueChecker_2...
[ OK ] test_LeaqueChecker_2
Tests run: 10
- ok 10 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.25 sec
----------------------------------------------------------
Test Passed.
"Option" end time: Mar 19 03:04 CST
"Option" time elapsed: 00:00:00
----------------------------------------------------------
31/38 Testing: Stack
31/38 Test: Stack
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Stack"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Stack" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running stackDelIterator...
[ OK ] stackDelIterator
Tests run: 1
- ok 1 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.10 sec
----------------------------------------------------------
Test Passed.
"Stack" end time: Mar 19 03:04 CST
"Stack" time elapsed: 00:00:00
----------------------------------------------------------
32/38 Testing: Set
32/38 Test: Set
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Set"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Set" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running find_remove_contains...
[ OK ] find_remove_contains
Running reset...
[ OK ] reset
Running dummy_hash...
[ OK ] dummy_hash
Tests run: 3
- ok 3 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.14 sec
----------------------------------------------------------
Test Passed.
"Set" end time: Mar 19 03:04 CST
"Set" time elapsed: 00:00:00
----------------------------------------------------------
33/38 Testing: Deque
33/38 Test: Deque
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Deque"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Deque" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running push_front_pop_back_expand...
[ OK ] push_front_pop_back_expand
Running size_reset_desctructor...
[ OK ] size_reset_desctructor
Tests run: 2
- ok 2 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.12 sec
----------------------------------------------------------
Test Passed.
"Deque" end time: Mar 19 03:04 CST
"Deque" time elapsed: 00:00:00
----------------------------------------------------------
34/38 Testing: TermAlgebra
34/38 Test: TermAlgebra
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "TermAlgebra"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"TermAlgebra" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running excludeTermFromAvailables...
[ OK ] excludeTermFromAvailables
Running excludeNested...
[ OK ] excludeNested
Tests run: 2
- ok 2 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.14 sec
----------------------------------------------------------
Test Passed.
"TermAlgebra" end time: Mar 19 03:04 CST
"TermAlgebra" time elapsed: 00:00:00
----------------------------------------------------------
35/38 Testing: FunctionDefinitionHandler
35/38 Test: FunctionDefinitionHandler
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "FunctionDefinitionHandler"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"FunctionDefinitionHandler" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running test_01...
[ OK ] test_01
Running test_02...
[ OK ] test_02
Running test_03...
[ OK ] test_03
Running test_04...
[ OK ] test_04
Running test_05...
[ OK ] test_05
Running test_06...
[ OK ] test_06
Tests run: 6
- ok 6 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.42 sec
----------------------------------------------------------
Test Passed.
"FunctionDefinitionHandler" end time: Mar 19 03:04 CST
"FunctionDefinitionHandler" time elapsed: 00:00:00
----------------------------------------------------------
36/38 Testing: FunctionDefinitionRewriting
36/38 Test: FunctionDefinitionRewriting
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "FunctionDefinitionRewriting"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"FunctionDefinitionRewriting" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running test_00...
[ OK ] test_00
Running test_01...
[ OK ] test_01
Running test_02...
[ OK ] test_02
Running test_03...
[ OK ] test_03
Running test_04...
[ OK ] test_04
Running test_05...
[ OK ] test_05
Running test_06...
[ OK ] test_06
Tests run: 7
- ok 7 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 0.53 sec
----------------------------------------------------------
Test Passed.
"FunctionDefinitionRewriting" end time: Mar 19 03:04 CST
"FunctionDefinitionRewriting" time elapsed: 00:00:00
----------------------------------------------------------
37/38 Testing: TheoryInstAndSimp
37/38 Test: TheoryInstAndSimp
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "TheoryInstAndSimp"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"TheoryInstAndSimp" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running test_01...
[Z3] solve result: sat
[Z3] add (naming): (= v4 (< |c'$inst0'| |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v3 (< 0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 6 (* |c'$inst0'| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 1 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_01
Running test_02...
[Z3] solve result: sat
[Z3] add (naming): (= v5 ((_ is cons) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v6 ((_ is cons) |c'$inst2'|))
[Z3] solve result: sat
[Z3] add (naming): (= v5 ((_ is cons) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v6 ((_ is cons) |c'$inst2'|))
[Z3] solve result: sat
[Z3] add (naming): (= v5 ((_ is cons) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v4 (= nil (|'cons@1'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v3 (= 1 (|'cons@0'_$| |c'$inst2'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 0 (|'cons@0'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= (|'cons@1'_$| |c'$inst1'|) (|'cons@1'_$| |c'$inst2'|)))
[Z3] solve result: sat
[ OK ] test_02
Running test_03...
[ OK ] test_03
Running test_04...
[ OK ] test_04
Running test_05...
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 7.0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0.0 (+ |c'$inst0'| |c'$inst1'|)))
[Z3] solve result: sat
[ OK ] test_05
Running test_06...
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 7.0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= (+ |c'$inst0'| |c'$inst1'|) (* 0.0 |c'$inst2'|)))
[Z3] solve result: sat
[ OK ] test_06
Running test_07...
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 7.0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= (+ |c'$inst0'| |c'$inst1'|) (* 0.0 |c'$inst2'|)))
[Z3] solve result: sat
[ OK ] test_07
Running test_08...
[Z3] solve result: sat
[Z3] add (naming): (= v3 (= 1 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 1))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_08
Running test_09...
[Z3] solve result: sat
[Z3] add (naming): (= v3 (= 0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 1))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_09
Running test_all_vs_strong_1a...
[Z3] solve result: sat
[Z3] add (naming): (= v2 (< |c'$inst0'| 1))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (< (- 1) |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_all_vs_strong_1a
Running test_all_vs_strong_1b...
[Z3] solve result: sat
[Z3] add (naming): (= v3 (= 0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (< |c'$inst0'| 1))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (< (- 1) |c'$inst0'|))
[Z3] solve result: unsat
[ OK ] test_all_vs_strong_1b
Running test_all_vs_strong_2a...
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 7 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_all_vs_strong_2a
Running test_all_vs_strong_2b...
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 7 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 7 |c'$inst0'|))
[Z3] solve result: unsat
[ OK ] test_all_vs_strong_2b
Running test_overlap_vs_strong_1a...
[Z3] solve result: sat
[Z3] add (naming): (= v3 (= 0 |c'$inst0'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 0))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: unsat
[ OK ] test_overlap_vs_strong_1a
Running test_overlap_vs_strong_1b...
[Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 0))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_overlap_vs_strong_1b
Running test_overlap_vs_strong_2...
[Z3] solve result: sat
[Z3] add (naming): (= v2 (<= |c'$inst0'| 0))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (<= 0 |c'$inst0'|))
[Z3] solve result: sat
[ OK ] test_overlap_vs_strong_2
Running bug_01...
[Z3] solve result: sat
[Z3] add (naming): (= v2 ((_ is pair) (pair 0 127)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0 (|'pair@0'_$| (pair 0 127))))
[Z3] solve result: unsat
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0 (|'pair@0'_$| (pair 0 127))))
[Z3] solve result: unsat
[ OK ] bug_01
Running bug_02...
[Z3] solve result: sat
[Z3] add (naming): (= v2 ((_ is cons) nil))
[Z3] solve result: unsat
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= nil (|'cons@1'_$| nil)))
[Z3] solve result: sat
[ OK ] bug_02
Running bug_03...
[Z3] solve result: sat
[Z3] add (naming): (= v2 ((_ is pair) (pair 0 127)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0 (|'pair@0'_$| (pair 0 127))))
[Z3] solve result: sat
[ OK ] bug_03
Running bug_04...
[Z3] add (naming): (= v1 (= nil (|'cons@1'_$| nil)))
[Z3] add (naming): (= v2 ((_ is cons) nil))
[Z3] solve result: unsat
[Z3] add (naming): (= v1 (= nil (|'cons@1'_$| nil)))
[Z3] solve result: sat
[ OK ] bug_04
Running pair_1...
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v2 (= 10 (|'pair@0'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v1 (= 0 (+ (|'pair@0'_$| |c'$inst1'|) (|'pair@1'_$| |c'$inst1'|))))
[Z3] solve result: sat
[ OK ] pair_1
Running generalisation_1...
[Z3] add (naming): (= v1 (= 10 (|'pair@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 ((_ is pair) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (clause): (or false v0 v3)
[Z3] add (naming): (= v3 (= 10 |c'$inst$gen2'|))
[Z3] add (naming): (= v4 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v5 (= |c'$inst1'| (pair |c'$inst$gen2'| |c'$inst$gen3'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-4455f1476f9f25fbcd8bb03b98a0cbc0f1d99c91/Inferences/TheoryInstAndSimp.cpp, line 566 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x11fb8c 0xaa17bc 0xaa0a28 0xaa0c0c 0xaa12b8 0xaa0f20 0xaa146c 0x38c048 0x38f698 0x70b5b4 0x70961c 0x70921c 0x70c0ec 0x708ebc 0x3248a8 0x3c518
invoking atos(1) ...
sh: /usr/bin/atos: Permission denied
[ FAIL ] generalisation_1
Running generalisation_2...
[Z3] add (naming): (let ((a!1 (= 10
(+ (|'cons@0'_$| |c'$inst1'|)
(|'cons@0'_$| (|'cons@1'_$| |c'$inst1'|))))))
(= v1 a!1))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v3 ((_ is cons) |c'$inst1'|))
[Z3] add (naming): (= v4 ((_ is cons) (|'cons@1'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is cons) |c'$inst1'|))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (clause): (or false v0 v3 v2 v5 v2 v2)
[Z3] add (naming): (= v5 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v6 (= 8 |c'$inst$gen5'|))
[Z3] add (naming): (= v7 (= nil |c'$inst$gen6'|))
[Z3] add (naming): (= v8 (= |c'$inst$gen4'| (cons |c'$inst$gen5'| |c'$inst$gen6'|)))
[Z3] add (naming): (= v9 (= |c'$inst1'| (cons |c'$inst$gen3'| |c'$inst$gen4'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-4455f1476f9f25fbcd8bb03b98a0cbc0f1d99c91/Inferences/TheoryInstAndSimp.cpp, line 566 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x11fb8c 0xaa17bc 0xaa0a28 0xaa0c0c 0xaa12b8 0xaa0f20 0xaa146c 0x38c984 0x38f698 0x70b5b4 0x70961c 0x70921c 0x70c0ec 0x708ebc 0x3248a8 0x3c518
invoking atos(1) ...
sh: /usr/bin/atos: Permission denied
[ FAIL ] generalisation_2
Running generalisation_3...
[Z3] add (naming): (let ((a!1 (+ (|'cons@0'_$| |c'$inst1'|)
(|'cons@0'_$| (|'cons@1'_$| (|'cons@1'_$| |c'$inst1'|))))))
(= v1 (= 10 a!1)))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v3 ((_ is cons) |c'$inst1'|))
[Z3] add (naming): (= v4 ((_ is cons) (|'cons@1'_$| (|'cons@1'_$| |c'$inst1'|))))
[Z3] add (naming): (= v5 ((_ is cons) (|'cons@1'_$| |c'$inst1'|)))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is cons) |c'$inst1'|))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v5 ((_ is cons) (|'cons@1'_$| |c'$inst1'|)))
[Z3] add (naming): (= v4 ((_ is cons) (|'cons@1'_$| (|'cons@1'_$| |c'$inst1'|))))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 (= 2 (|'cons@0'_$| |c'$inst1'|)))
[Z3] add (clause): (or false v0 v3 v2 v5 v4 v2 v2)
[Z3] add (naming): (= v6 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v7 (= 3 |c'$inst$gen5'|))
[Z3] add (naming): (= v8 (= 8 |c'$inst$gen7'|))
[Z3] add (naming): (= v9 (= nil |c'$inst$gen8'|))
[Z3] add (naming): (= v10 (= |c'$inst$gen6'| (cons |c'$inst$gen7'| |c'$inst$gen8'|)))
[Z3] add (naming): (= v11 (= |c'$inst$gen4'| (cons |c'$inst$gen5'| |c'$inst$gen6'|)))
[Z3] add (naming): (= v12 (= |c'$inst1'| (cons |c'$inst$gen3'| |c'$inst$gen4'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-4455f1476f9f25fbcd8bb03b98a0cbc0f1d99c91/Inferences/TheoryInstAndSimp.cpp, line 566 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x11fb8c 0xaa17bc 0xaa0a28 0xaa0c0c 0xaa12b8 0xaa0f20 0xaa146c 0x38d3f0 0x38f698 0x70b5b4 0x70961c 0x70921c 0x70c0ec 0x708ebc 0x3248a8 0x3c518
invoking atos(1) ...
sh: /usr/bin/atos: Permission denied
[ FAIL ] generalisation_3
Running generalisation_4...
[Z3] add (naming): (= v1 (= nil (|'cons@1'_$| |c'$inst1'|)))
[Z3] add (naming): (= v2 ((_ is cons) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (clause): (or false (not v0) v3)
[Z3] add (naming): (= v3 (= 2 |c'$inst$gen3'|))
[Z3] add (naming): (= v4 (= 3 |c'$inst$gen5'|))
[Z3] add (naming): (= v5 (= nil |c'$inst$gen6'|))
[Z3] add (naming): (= v6 (= |c'$inst$gen4'| (cons |c'$inst$gen5'| |c'$inst$gen6'|)))
[Z3] add (naming): (= v7 (= |c'$inst1'| (cons |c'$inst$gen3'| |c'$inst$gen4'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-4455f1476f9f25fbcd8bb03b98a0cbc0f1d99c91/Inferences/TheoryInstAndSimp.cpp, line 566 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x11fb8c 0xaa17bc 0xaa0a28 0xaa0c0c 0xaa12b8 0xaa0f20 0xaa146c 0x38dd74 0x38f698 0x70b5b4 0x70961c 0x70921c 0x70c0ec 0x708ebc 0x3248a8 0x3c518
invoking atos(1) ...
sh: /usr/bin/atos: Permission denied
[ FAIL ] generalisation_4
Running generalisation_5...
[Z3] add (naming): (= v1 (= zero (|'s@0'_$| (|'s@0'_$| |c'$inst1'|))))
[Z3] add (naming): (= v2 ((_ is s) (|'s@0'_$| |c'$inst1'|)))
[Z3] add (naming): (= v3 ((_ is s) |c'$inst1'|))
[Z3] solve result: sat
[Z3] add (naming): (= v3 ((_ is s) |c'$inst1'|))
[Z3] add (naming): (= v2 ((_ is s) (|'s@0'_$| |c'$inst1'|)))
[Z3] add (clause): (or false (not v0) v3 v2)
[Z3] add (naming): (= v4 (= zero |c'$inst$gen5'|))
[Z3] add (naming): (= v5 (= |c'$inst$gen4'| (s |c'$inst$gen5'|)))
[Z3] add (naming): (= v6 (= |c'$inst$gen3'| (s |c'$inst$gen4'|)))
[Z3] add (naming): (= v7 (= |c'$inst1'| (s |c'$inst$gen3'|)))
[Z3] solve result: sat
Condition res == SATSolver::UNSATISFIABLE in file /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/vampire-4455f1476f9f25fbcd8bb03b98a0cbc0f1d99c91/Inferences/TheoryInstAndSimp.cpp, line 566 was violated, as:
res == SATISFIABLE
SATSolver::UNSATISFIABLE == UNSATISFIABLE
----- stack dump -----
Version : Vampire 4.8 (commit )
call stack: 0x11fb8c 0xaa17bc 0xaa0a28 0xaa0c0c 0xaa12b8 0xaa0f20 0xaa146c 0x38e4f4 0x38f698 0x70b5b4 0x70961c 0x70921c 0x70c0ec 0x708ebc 0x3248a8 0x3c518
invoking atos(1) ...
sh: /usr/bin/atos: Permission denied
[ FAIL ] generalisation_5
Tests run: 26
- ok 21 (80.8) %
- fail 5 (19.2) %
<end of output>
Test time = 8.12 sec
----------------------------------------------------------
Test Failed.
"TheoryInstAndSimp" end time: Mar 19 03:04 CST
"TheoryInstAndSimp" time elapsed: 00:00:08
----------------------------------------------------------
38/38 Testing: Z3Interfacing
38/38 Test: Z3Interfacing
Command: "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build/vtest" "run" "Z3Interfacing"
Directory: /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
"Z3Interfacing" start time: Mar 19 03:04 CST
Output:
----------------------------------------------------------
Running solve__real__simple_01...
[Z3] add (naming): (= v1 (= 3.0 0.0))
[Z3] solve result: unsat
[ OK ] solve__real__simple_01
Running solve__real__simple_02...
[Z3] add (naming): (= v1 (= ca 3.0))
[Z3] solve result: sat
[ OK ] solve__real__simple_02
Running solve__rat__simple_03...
[Z3] add (naming): (= v1 (= 3.0 (+ 3.0 (* 2.0 7.0))))
[Z3] solve result: unsat
[ OK ] solve__rat__simple_03
Running solve__rat__simple_04...
[Z3] add (naming): (= v1 (= 17.0 (+ 3.0 (* 2.0 7.0))))
[Z3] solve result: unsat
[ OK ] solve__rat__simple_04
Running solve__fool__simple_01...
[Z3] solve result: sat
[ OK ] solve__fool__simple_01
Running solve__fool__simple_02...
[Z3] solve result: sat
[ OK ] solve__fool__simple_02
Running solve__fool__simple_03...
[Z3] add (naming): (= v1 (= true false))
[Z3] solve result: unsat
[ OK ] solve__fool__simple_03
Running solve__dty__01...
[Z3] add (naming): (= v1 (= nil (cons ca0 nil)))
[Z3] solve result: unsat
[Z3] add (naming): (= v1 (= (cons ca0 nil) (cons ca1 nil)))
[Z3] add (naming): (= v2 (= ca0 ca1))
[Z3] solve result: unsat
[ OK ] solve__dty__01
Running solve__dty__02...
[Z3] add (naming): (= v1 (= zero (succEven (succOdd zero))))
[Z3] solve result: unsat
[ OK ] solve__dty__02
Running solve__dty__03_01...
[Z3] add (naming): (let ((a!1 (= (cons (succEven (succOdd zero)) nil) (cons zero nil))))
(= v1 a!1))
[Z3] solve result: unsat
[ OK ] solve__dty__03_01
Running solve__dty__03_02...
[Z3] add (naming): (= v1 (= zero (succEven (succOdd zero))))
[Z3] solve result: unsat
[ OK ] solve__dty__03_02
Running solve__dty__03_03...
[Z3] add (naming): (= v1 (= zero (succEven (succOdd zero))))
[Z3] solve result: unsat
[Z3] add (naming): (let ((a!1 (= (cons (succEven (succOdd zero)) nil) (cons zero nil))))
(= v1 a!1))
[Z3] solve result: unsat
[ OK ] solve__dty__03_03
Running instantiate__rat__simple_01...
[Z3] add (naming): (= v1 (= (* cc 3.0) 9.0))
[Z3] solve result: sat
[ OK ] instantiate__rat__simple_01
Running instantiate__rat__simple_02...
[Z3] add (naming): (= v1 (= (* cc cc) 9.0))
[Z3] add (naming): (= v2 (< cc 0.0))
[Z3] solve result: sat
[ OK ] instantiate__rat__simple_02
Running instantiate__list_01...
[Z3] add (naming): (= v1 (= (cons cc nil) (cons 3.0 nil)))
[Z3] solve result: sat
[ OK ] instantiate__list_01
Running instantiate__list_02...
[Z3] add (naming): (= v1 (= (|'cons@1'_$| cl) (cons 2.0 nil)))
[Z3] add (naming): (= v2 (= (|'cons@0'_$| cl) 1.0))
[Z3] add (naming): (= v3 (= cl (cons ch ct)))
[Z3] solve result: sat
[ OK ] instantiate__list_02
Running segfault01...
[ OK ] segfault01
Running segfault02...
[Z3] add (naming): (= v1 (= cinst159 cinst160))
[Z3] solve result: sat
[Z3] solve result: sat
[ OK ] segfault02
Tests run: 18
- ok 18 (100.0) %
- fail 0 (0.0) %
<end of output>
Test time = 3.62 sec
----------------------------------------------------------
Test Passed.
"Z3Interfacing" end time: Mar 19 03:04 CST
"Z3Interfacing" time elapsed: 00:00:03
----------------------------------------------------------
End testing: Mar 19 03:04 CST
MichaelRawson commented
Thanks for testing! That patch has now been merged so things ought to improve at least. I don't think there's anything else as bad in Vampire; there is similar pointer-tagging horror here, but it's much less frequently used. Will also fix in time.
The failing test case is not a good sign, but it relies on Z3 - do you know if Z3 works on PowerPC? If not, let's disable Z3 first so that we only get failing test cases "from Vampire". Could you re-build without Z3? (you can pass -DCMAKE_DISABLE_FIND_PACKAGE_Z3=ON to CMake)
JakobR commented
Z3 does use some pointer tagging magic (see https://github.com/Z3Prover/z3/blob/master/src/util/tptr.h; maybe not the only place, but the only one I know of). But I think what Z3 does only depends on alignment and not on endianness.
barracuda156 commented
@JakobR With 4-byte bools and spinlocks there are chances alignment gets wrong.
MichaelRawson commented
Is /usr/bin/atos anything consequential? For some reason it is not allowed:
Also realised I failed to respond to this bit - it's not consequential, it's just how we do tracebacks in a pinch. See Debug/Tracer.hpp.
Not sure why you'd get "permission denied" from trying to run it, but I'm not a Mac expert.
MichaelRawson commented
#543 also fixed the more-obscure bitfields in Vampire in a similar way. We might now be OK without Z3, if you can find something that doesn't work with a non-Z3 build let us know!
barracuda156 commented
@MichaelRawson Thank you! Sorry for a delay, I will build and run tests now from the master and disabling Z3.
barracuda156 commented
From c7564c1 and without Z3:
---> Testing vampire
Executing: cd "/opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build" && ninja test
[0/1] Running tests...
Test project /opt/local/var/macports/build/_opt_PPCSnowLeopardPorts_math_vampire/vampire/work/build
Start 1: DHMap
1/37 Test #1: DHMap ............................. Passed 0.13 sec
Start 2: QuotientE
2/37 Test #2: QuotientE ......................... Passed 0.41 sec
Start 3: UnificationWithAbstraction
3/37 Test #3: UnificationWithAbstraction ........ Passed 2.04 sec
Start 4: TermIndex
4/37 Test #4: TermIndex ......................... Passed 0.33 sec
Start 5: GaussianElimination
5/37 Test #5: GaussianElimination ............... Passed 0.67 sec
Start 6: PushUnaryMinus
6/37 Test #6: PushUnaryMinus .................... Passed 0.22 sec
Start 7: ArithmeticSubtermGeneralization
7/37 Test #7: ArithmeticSubtermGeneralization ... Passed 5.95 sec
Start 8: InterpretedFunctions
8/37 Test #8: InterpretedFunctions .............. Passed 8.72 sec
Start 9: Rebalance
9/37 Test #9: Rebalance ......................... Passed 1.43 sec
Start 10: Disagreement
10/37 Test #10: Disagreement ...................... Passed 0.11 sec
Start 11: DynamicHeap
11/37 Test #11: DynamicHeap ....................... Passed 0.15 sec
Start 12: Induction
12/37 Test #12: Induction ......................... Passed 3.89 sec
Start 13: IntegerConstantType
13/37 Test #13: IntegerConstantType ............... Passed 0.10 sec
Start 14: SATSolver
14/37 Test #14: SATSolver ......................... Passed 0.14 sec
Start 15: ArithCompare
15/37 Test #15: ArithCompare ...................... Passed 0.10 sec
Start 16: SyntaxSugar
16/37 Test #16: SyntaxSugar ....................... Passed 0.26 sec
Start 17: SkipList
17/37 Test #17: SkipList .......................... Passed 1.21 sec
Start 18: BinaryHeap
18/37 Test #18: BinaryHeap ........................ Passed 0.12 sec
Start 19: SafeRecursion
19/37 Test #19: SafeRecursion ..................... Passed 0.13 sec
Start 20: KBO
20/37 Test #20: KBO ............................... Passed 0.75 sec
Start 21: SKIKBO
21/37 Test #21: SKIKBO ............................ Passed 0.23 sec
Start 22: LPO
22/37 Test #22: LPO ............................... Passed 0.20 sec
Start 23: RatioKeeper
23/37 Test #23: RatioKeeper ....................... Passed 0.10 sec
Start 24: OptionConstraints
24/37 Test #24: OptionConstraints ................. Passed 0.26 sec
Start 25: DHMultiset
25/37 Test #25: DHMultiset ........................ Passed 0.21 sec
Start 26: List
26/37 Test #26: List .............................. Passed 0.10 sec
Start 27: BottomUpEvaluation
27/37 Test #27: BottomUpEvaluation ................ Passed 0.13 sec
Start 28: Coproduct
28/37 Test #28: Coproduct ......................... Passed 0.29 sec
Start 29: EqualityResolution
29/37 Test #29: EqualityResolution ................ Passed 0.35 sec
Start 30: Iterator
30/37 Test #30: Iterator .......................... Passed 0.20 sec
Start 31: Option
31/37 Test #31: Option ............................ Passed 0.25 sec
Start 32: Stack
32/37 Test #32: Stack ............................. Passed 0.10 sec
Start 33: Set
33/37 Test #33: Set ............................... Passed 0.14 sec
Start 34: Deque
34/37 Test #34: Deque ............................. Passed 0.12 sec
Start 35: TermAlgebra
35/37 Test #35: TermAlgebra ....................... Passed 0.14 sec
Start 36: FunctionDefinitionHandler
36/37 Test #36: FunctionDefinitionHandler ......... Passed 0.39 sec
Start 37: FunctionDefinitionRewriting
37/37 Test #37: FunctionDefinitionRewriting ....... Passed 0.51 sec
100% tests passed, 0 tests failed out of 37
Total Test time (real) = 30.68 sec
MichaelRawson commented
Nice! The unit tests aren't particularly exhaustive, but that's a good sign. Let's consider this closed: feel free to open new issues with new PowerPC bugs.
barracuda156 commented
@MichaelRawson By the way, what is the status on aarch64? I ran tests on Sonoma, and 3 tests failed:
92% tests passed, 3 tests failed out of 37
Total Test time (real) = 2.78 sec
The following tests FAILED:
8 - InterpretedFunctions (Failed)
20 - KBO (Failed)
24 - OptionConstraints (Failed)
(I can open a new issue if this is not something known already.)
MichaelRawson commented
(I can open a new issue if this is not something known already.)
I know nothing about it! Please do open the issue.
barracuda156 commented
(I can open a new issue if this is not something known already.)
I know nothing about it! Please do open the issue.
Done: #545