Go to:
Gentoo Home
Documentation
Forums
Lists
Bugs
Planet
Store
Wiki
Get Gentoo!
Gentoo's Bugzilla – Attachment 904423 Details for
Bug 940574
sci-mathematics/vampire-4.9 fails tests: 3 - UnificationWithAbstraction (Failed)
Home
|
New
–
[Ex]
|
Browse
|
Search
|
Privacy Policy
|
[?]
|
Reports
|
Requests
|
Help
|
New Account
|
Log In
[x]
|
Forgot Password
Login:
[x]
1-LastTest.log
1-LastTest.log (text/plain), 86.91 KB, created by
Agostino Sarubbo
on 2024-10-01 06:43:46 UTC
(
hide
)
Description:
1-LastTest.log
Filename:
MIME Type:
Creator:
Agostino Sarubbo
Created:
2024-10-01 06:43:46 UTC
Size:
86.91 KB
patch
obsolete
>Start testing: Sep 30 20:32 CEST >---------------------------------------------------------- >1/39 Testing: DHMap >1/39 Test: DHMap >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "DHMap" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"DHMap" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running dhmap1... [ OK ] dhmap1 > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.07 sec >---------------------------------------------------------- >Test Passed. >"DHMap" end time: Sep 30 20:32 CEST >"DHMap" time elapsed: 00:00:00 >---------------------------------------------------------- > >2/39 Testing: QuotientE >2/39 Test: QuotientE >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "QuotientE" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"QuotientE" start time: Sep 30 20:32 CEST >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.07 sec >---------------------------------------------------------- >Test Passed. >"QuotientE" end time: Sep 30 20:32 CEST >"QuotientE" time elapsed: 00:00:00 >---------------------------------------------------------- > >4/39 Testing: TermIndex >4/39 Test: TermIndex >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "TermIndex" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"TermIndex" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running basic01... [ ok ] unify f(a): srt >[ ok ] unify f(b): srt >[ ok ] unify f(X0): srt > [ OK ] basic01 >Running custom_data_01... [ ok ] unify f(a): srt >[ ok ] unify f(b): srt >[ ok ] unify f(X0): srt > [ OK ] custom_data_01 >Running custom_data_literal_01... [ ok ] unify p(a) >[ ok ] unify ~(p(a)) >[ ok ] unify ~(p(a)) >[ ok ] unify p(a) >[ ok ] unify p(b) >[ ok ] unify ~(p(b)) >[ ok ] unify ~(p(b)) >[ ok ] unify p(b) >[ ok ] unify p(X0) >[ ok ] unify ~(p(X0)) >[ ok ] unify ~(p(X0)) >[ ok ] unify p(X0) > [ OK ] custom_data_literal_01 >Running custom_data_02... [ ok ] unify f(a): srt >[ ok ] unify f(b): srt >[ ok ] unify f(X0): srt > [ OK ] custom_data_02 >Running custom_data_03_no_default_constructor... [ ok ] unify f(a): srt >[ ok ] unify f(b): srt >[ ok ] unify f(X0): srt > [ OK ] custom_data_03_no_default_constructor >Running custom_data_04_no_copy_constructor... [ ok ] unify f(a): srt >[ ok ] unify f(b): srt >[ ok ] unify f(X0): srt >[ ok ] unify f(a): srt >[ ok ] unify f(b): srt >[ ok ] unify f(X0): srt > [ OK ] custom_data_04_no_copy_constructor >Running zero_arity_predicate... [ ok ] unify p0 >[ ok ] unify ~(p0) >[ ok ] unify p1(X0) >[ ok ] unify ~(p1(X0)) >[ ok ] unify ~(p0) >[ ok ] unify p0 >[ ok ] unify ~(p1(X0)) >[ ok ] unify p1(X0) >[ ok ] unify p1(a) >[ ok ] unify ~(p1(a)) >[ ok ] unify ~(p1(a)) >[ ok ] unify p1(a) >[ ok ] unify p1(X0) >[ ok ] unify ~(p1(X0)) >[ ok ] unify ~(p1(X0)) >[ ok ] unify p1(X0) >[ ok ] getInst p1(X0) >[ ok ] getInst ~(p1(X0)) >[ ok ] getInst ~(p1(X0)) >[ ok ] getInst p1(X0) >[ ok ] unify p0 >[ ok ] unify ~(p0) >[ ok ] unify ~(p0) >[ ok ] unify p0 >[ ok ] getGen p0 >[ ok ] getGen ~(p0) >[ ok ] getGen ~(p0) >[ ok ] getGen p0 >[ ok ] getInst p0 >[ ok ] getInst ~(p0) >[ ok ] getInst ~(p0) >[ ok ] getInst p0 >[ ok ] getGen p1(a) >[ ok ] getGen ~(p1(a)) >[ ok ] getGen ~(p1(a)) >[ ok ] getGen p1(a) >[ ok ] getGen ~((a = a)) >[ ok ] getGen (a = a) >[ ok ] getInst ~((a = a)) >[ ok ] getInst (a = a) >[ ok ] unify ~((a = a)) >[ ok ] unify (a = a) > [ OK ] zero_arity_predicate > >Tests run: 7 > - ok 7 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.07 sec >---------------------------------------------------------- >Test Passed. >"TermIndex" end time: Sep 30 20:32 CEST >"TermIndex" time elapsed: 00:00:00 >---------------------------------------------------------- > >5/39 Testing: GaussianElimination >5/39 Test: GaussianElimination >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "GaussianElimination" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"GaussianElimination" start time: Sep 30 20:32 CEST >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.06 sec >---------------------------------------------------------- >Test Passed. >"GaussianElimination" end time: Sep 30 20:32 CEST >"GaussianElimination" time elapsed: 00:00:00 >---------------------------------------------------------- > >6/39 Testing: PushUnaryMinus >6/39 Test: PushUnaryMinus >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "PushUnaryMinus" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"PushUnaryMinus" start time: Sep 30 20:32 CEST >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.06 sec >---------------------------------------------------------- >Test Passed. >"PushUnaryMinus" end time: Sep 30 20:32 CEST >"PushUnaryMinus" time elapsed: 00:00:00 >---------------------------------------------------------- > >10/39 Testing: Disagreement >10/39 Test: Disagreement >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Disagreement" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Disagreement" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running dis1... [ OK ] dis1 > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.06 sec >---------------------------------------------------------- >Test Passed. >"Disagreement" end time: Sep 30 20:32 CEST >"Disagreement" time elapsed: 00:00:00 >---------------------------------------------------------- > >11/39 Testing: DynamicHeap >11/39 Test: DynamicHeap >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "DynamicHeap" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"DynamicHeap" start time: Sep 30 20:32 CEST >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.05 sec >---------------------------------------------------------- >Test Passed. >"DynamicHeap" end time: Sep 30 20:32 CEST >"DynamicHeap" time elapsed: 00:00:00 >---------------------------------------------------------- > >13/39 Testing: IntegerConstantType >13/39 Test: IntegerConstantType >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "IntegerConstantType" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"IntegerConstantType" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running list_1... [ OK ] list_1 > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.05 sec >---------------------------------------------------------- >Test Passed. >"IntegerConstantType" end time: Sep 30 20:32 CEST >"IntegerConstantType" time elapsed: 00:00:00 >---------------------------------------------------------- > >14/39 Testing: SATSolver >14/39 Test: SATSolver >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "SATSolver" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"SATSolver" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running testProofWithAssums... [ OK ] testProofWithAssums >Running testSATSolverInterface... >Minisat > Random: 0011001011 Fixed: 1111111111 > [ OK ] testSATSolverInterface >Running testSolvingUnderAssumptions... >Minisat >CDE >CDE > [ OK ] testSolvingUnderAssumptions > >Tests run: 3 > - ok 3 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.05 sec >---------------------------------------------------------- >Test Passed. >"SATSolver" end time: Sep 30 20:32 CEST >"SATSolver" time elapsed: 00:00:00 >---------------------------------------------------------- > >15/39 Testing: ArithCompare >15/39 Test: ArithCompare >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "ArithCompare" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"ArithCompare" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running testArithCompareSAT... [ OK ] testArithCompareSAT > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.05 sec >---------------------------------------------------------- >Test Passed. >"ArithCompare" end time: Sep 30 20:32 CEST >"ArithCompare" time elapsed: 00:00:00 >---------------------------------------------------------- > >16/39 Testing: SyntaxSugar >16/39 Test: SyntaxSugar >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "SyntaxSugar" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"SyntaxSugar" start time: Sep 30 20:32 CEST >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.05 sec >---------------------------------------------------------- >Test Passed. >"SyntaxSugar" end time: Sep 30 20:32 CEST >"SyntaxSugar" time elapsed: 00:00:00 >---------------------------------------------------------- > >18/39 Testing: BinaryHeap >18/39 Test: BinaryHeap >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "BinaryHeap" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"BinaryHeap" start time: Sep 30 20:32 CEST >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.04 sec >---------------------------------------------------------- >Test Passed. >"BinaryHeap" end time: Sep 30 20:32 CEST >"BinaryHeap" time elapsed: 00:00:00 >---------------------------------------------------------- > >19/39 Testing: SafeRecursion >19/39 Test: SafeRecursion >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "SafeRecursion" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"SafeRecursion" start time: Sep 30 20:32 CEST >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.04 sec >---------------------------------------------------------- >Test Passed. >"SafeRecursion" end time: Sep 30 20:32 CEST >"SafeRecursion" time elapsed: 00:00:00 >---------------------------------------------------------- > >21/39 Testing: SKIKBO >21/39 Test: SKIKBO >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "SKIKBO" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"SKIKBO" start time: Sep 30 20:32 CEST >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.04 sec >---------------------------------------------------------- >Test Passed. >"SKIKBO" end time: Sep 30 20:32 CEST >"SKIKBO" time elapsed: 00:00:00 >---------------------------------------------------------- > >22/39 Testing: LPO >22/39 Test: LPO >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "LPO" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"LPO" start time: Sep 30 20:32 CEST >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.04 sec >---------------------------------------------------------- >Test Passed. >"LPO" end time: Sep 30 20:32 CEST >"LPO" time elapsed: 00:00:00 >---------------------------------------------------------- > >23/39 Testing: RatioKeeper >23/39 Test: RatioKeeper >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "RatioKeeper" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"RatioKeeper" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running rkeeper1... [ OK ] rkeeper1 > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.03 sec >---------------------------------------------------------- >Test Passed. >"RatioKeeper" end time: Sep 30 20:32 CEST >"RatioKeeper" time elapsed: 00:00:00 >---------------------------------------------------------- > >24/39 Testing: OptionConstraints >24/39 Test: OptionConstraints >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "OptionConstraints" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"OptionConstraints" start time: Sep 30 20:32 CEST >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.03 sec >---------------------------------------------------------- >Test Passed. >"OptionConstraints" end time: Sep 30 20:32 CEST >"OptionConstraints" time elapsed: 00:00:00 >---------------------------------------------------------- > >25/39 Testing: DHMultiset >25/39 Test: DHMultiset >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "DHMultiset" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"DHMultiset" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running dhmultiset1... [ OK ] dhmultiset1 > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.03 sec >---------------------------------------------------------- >Test Passed. >"DHMultiset" end time: Sep 30 20:32 CEST >"DHMultiset" time elapsed: 00:00:00 >---------------------------------------------------------- > >26/39 Testing: List >26/39 Test: List >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "List" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"List" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running list1... [ OK ] list1 > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.03 sec >---------------------------------------------------------- >Test Passed. >"List" end time: Sep 30 20:32 CEST >"List" time elapsed: 00:00:00 >---------------------------------------------------------- > >27/39 Testing: BottomUpEvaluation >27/39 Test: BottomUpEvaluation >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "BottomUpEvaluation" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"BottomUpEvaluation" start time: Sep 30 20:32 CEST >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.03 sec >---------------------------------------------------------- >Test Passed. >"BottomUpEvaluation" end time: Sep 30 20:32 CEST >"BottomUpEvaluation" time elapsed: 00:00:00 >---------------------------------------------------------- > >28/39 Testing: Coproduct >28/39 Test: Coproduct >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Coproduct" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Coproduct" start time: Sep 30 20:32 CEST >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.03 sec >---------------------------------------------------------- >Test Passed. >"Coproduct" end time: Sep 30 20:32 CEST >"Coproduct" time elapsed: 00:00:00 >---------------------------------------------------------- > >29/39 Testing: EqualityResolution >29/39 Test: EqualityResolution >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "EqualityResolution" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"EqualityResolution" start time: Sep 30 20:32 CEST >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.02 sec >---------------------------------------------------------- >Test Passed. >"EqualityResolution" end time: Sep 30 20:32 CEST >"EqualityResolution" time elapsed: 00:00:00 >---------------------------------------------------------- > >30/39 Testing: Iterator >30/39 Test: Iterator >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Iterator" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Iterator" start time: Sep 30 20:32 CEST >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.02 sec >---------------------------------------------------------- >Test Passed. >"Iterator" end time: Sep 30 20:32 CEST >"Iterator" time elapsed: 00:00:00 >---------------------------------------------------------- > >32/39 Testing: Stack >32/39 Test: Stack >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Stack" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Stack" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running stackDelIterator... [ OK ] stackDelIterator > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.02 sec >---------------------------------------------------------- >Test Passed. >"Stack" end time: Sep 30 20:32 CEST >"Stack" time elapsed: 00:00:00 >---------------------------------------------------------- > >33/39 Testing: Set >33/39 Test: Set >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Set" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Set" start time: Sep 30 20:32 CEST >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.02 sec >---------------------------------------------------------- >Test Passed. >"Set" end time: Sep 30 20:32 CEST >"Set" time elapsed: 00:00:00 >---------------------------------------------------------- > >34/39 Testing: Deque >34/39 Test: Deque >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Deque" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Deque" start time: Sep 30 20:32 CEST >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.02 sec >---------------------------------------------------------- >Test Passed. >"Deque" end time: Sep 30 20:32 CEST >"Deque" time elapsed: 00:00:00 >---------------------------------------------------------- > >35/39 Testing: TermAlgebra >35/39 Test: TermAlgebra >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "TermAlgebra" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"TermAlgebra" start time: Sep 30 20:32 CEST >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.01 sec >---------------------------------------------------------- >Test Passed. >"TermAlgebra" end time: Sep 30 20:32 CEST >"TermAlgebra" time elapsed: 00:00:00 >---------------------------------------------------------- > >31/39 Testing: Option >31/39 Test: Option >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Option" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Option" start time: Sep 30 20:32 CEST >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.02 sec >---------------------------------------------------------- >Test Passed. >"Option" end time: Sep 30 20:32 CEST >"Option" time elapsed: 00:00:00 >---------------------------------------------------------- > >36/39 Testing: FunctionDefinitionHandler >36/39 Test: FunctionDefinitionHandler >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "FunctionDefinitionHandler" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"FunctionDefinitionHandler" start time: Sep 30 20:32 CEST >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.02 sec >---------------------------------------------------------- >Test Passed. >"FunctionDefinitionHandler" end time: Sep 30 20:32 CEST >"FunctionDefinitionHandler" time elapsed: 00:00:00 >---------------------------------------------------------- > >37/39 Testing: FunctionDefinitionRewriting >37/39 Test: FunctionDefinitionRewriting >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "FunctionDefinitionRewriting" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"FunctionDefinitionRewriting" start time: Sep 30 20:32 CEST >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.02 sec >---------------------------------------------------------- >Test Passed. >"FunctionDefinitionRewriting" end time: Sep 30 20:32 CEST >"FunctionDefinitionRewriting" time elapsed: 00:00:00 >---------------------------------------------------------- > >20/39 Testing: KBO >20/39 Test: KBO >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "KBO" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"KBO" start time: Sep 30 20:32 CEST >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 >Running kbo_isGreater_test01... [ OK ] kbo_isGreater_test01 >Running kbo_isGreater_test02... [ OK ] kbo_isGreater_test02 >Running kbo_isGreater_test03... [ OK ] kbo_isGreater_test03 >Running kbo_isGreater_test04... [ OK ] kbo_isGreater_test04 >Running kbo_isGreater_test05... [ OK ] kbo_isGreater_test05 >Running kbo_isGreater_test06... [ OK ] kbo_isGreater_test06 >Running kbo_isGreater_test07... [ OK ] kbo_isGreater_test07 >Running kbo_isGreater_test08... [ OK ] kbo_isGreater_test08 >Running kbo_isGreater_test09... [ OK ] kbo_isGreater_test09 >Running kbo_isGreater_test10... [ OK ] kbo_isGreater_test10 >Running kbo_isGreater_test11... [ OK ] kbo_isGreater_test11 >Running kbo_isGreater_test12... [ OK ] kbo_isGreater_test12 >Running kbo_isGreater_test13... [ OK ] kbo_isGreater_test13 >Running kbo_isGreater_test14... [ OK ] kbo_isGreater_test14 >Running kbo_isGreater_test15... [ OK ] kbo_isGreater_test15 >Running kbo_isGreater_test16... [ OK ] kbo_isGreater_test16 >Running kbo_isGreater_test17... [ OK ] kbo_isGreater_test17 > >Tests run: 40 > - ok 40 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.05 sec >---------------------------------------------------------- >Test Passed. >"KBO" end time: Sep 30 20:32 CEST >"KBO" time elapsed: 00:00:00 >---------------------------------------------------------- > >9/39 Testing: Rebalance >9/39 Test: Rebalance >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Rebalance" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Rebalance" start time: Sep 30 20:32 CEST >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 = 0.08 sec >---------------------------------------------------------- >Test Passed. >"Rebalance" end time: Sep 30 20:32 CEST >"Rebalance" time elapsed: 00:00:00 >---------------------------------------------------------- > >17/39 Testing: SkipList >17/39 Test: SkipList >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "SkipList" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"SkipList" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running skiplist1... [ OK ] skiplist1 > >Tests run: 1 > - ok 1 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.08 sec >---------------------------------------------------------- >Test Passed. >"SkipList" end time: Sep 30 20:32 CEST >"SkipList" time elapsed: 00:00:00 >---------------------------------------------------------- > >3/39 Testing: UnificationWithAbstraction >3/39 Test: UnificationWithAbstraction >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "UnificationWithAbstraction" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"UnificationWithAbstraction" start time: Sep 30 20:32 CEST >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... [ FAIL ] f3(vAPP(srt > srt,srt,h,f2),X1,X1): srt >tree: S0 -> f3(X0,X0,vAPP(srt > srt,srt,h,f1)) ; S1 -> srt >query: f3(vAPP(srt > srt,srt,h,f2),X1,X1): srt >is: > { querySigma = f3(vAPP(h, f2, h, f2), vAPP(h, f2, h, f1), vAPP(h, f2, h, f1)), resultSigma = f3(vAPP(h, f2, h, f1), vAPP(h, f2, h, f1), vAPP(h, f2, h, f1)), cons = [ ] } >expected: > { querySigma = f3(vAPP(h, f2, h, f2), vAPP(h, f2, h, f1), vAPP(h, f2, h, f1)), resultSigma = f3(vAPP(h, f2, h, f1), vAPP(h, f2, h, f1), vAPP(h, f2, h, f1)), cons = [ (f1 != f2), ] } > [ FAIL ] hol_0101 >Running hol_0102... [ FAIL ] f3(X0,X0,vAPP(srt > srt,srt,h,f1)): srt >tree: S0 -> f3(vAPP(srt > srt,srt,h,f2),X0,X0) ; S1 -> srt >query: f3(X0,X0,vAPP(srt > srt,srt,h,f1)): srt >is: > { querySigma = f3(vAPP(h, f2, h, f1), vAPP(h, f2, h, f1), vAPP(h, f2, h, f1)), resultSigma = f3(vAPP(h, f2, h, f2), vAPP(h, f2, h, f1), vAPP(h, f2, h, f1)), cons = [ ] } >expected: > { querySigma = f3(vAPP(h, f2, h, f1), vAPP(h, f2, h, f1), vAPP(h, f2, h, f1)), resultSigma = f3(vAPP(h, f2, h, f2), vAPP(h, f2, h, f1), vAPP(h, f2, h, f1)), cons = [ (f1 != f2), ] } > [ FAIL ] hol_0102 >Running hol_02... [ FAIL ] f3(vAPP(srt > srt,srt,h,f2),X1,X1): srt >tree: S0 -> f3(S2,X0,vAPP(srt > srt,srt,h,f1)) ; S1 -> srt ; S2 -> [ > | a > | X0 > ] >query: f3(vAPP(srt > srt,srt,h,f2),X1,X1): srt >is: > { querySigma = f3(vAPP(a, f2, h, f2), vAPP(a, f2, h, f1), vAPP(a, f2, h, f1)), resultSigma = f3(vAPP(a, f2, h, f1), vAPP(a, f2, h, f1), vAPP(a, f2, h, f1)), cons = [ ] } >expected: > { querySigma = f3(vAPP(a, f2, h, f2), vAPP(a, f2, h, f1), vAPP(a, f2, h, f1)), resultSigma = f3(vAPP(a, f2, h, f1), vAPP(a, f2, h, f1), vAPP(a, f2, h, f1)), cons = [ (f1 != f2), ] } > [ FAIL ] hol_02 >Running hol_03... [ FAIL ] vAPP(srt > srt,srt,h1,f2): srt >tree: S0 -> vAPP(srt > srt,srt,S2,f1) ; S1 -> srt ; S2 -> [ > | h1 > | h2 > ] >query: vAPP(srt > srt,srt,h1,f2): srt >is: > { querySigma = vAPP(h1, f2, h1, f2), resultSigma = vAPP(h1, f2, h1, f1), cons = [ ] } >expected: > { querySigma = vAPP(h1, f2, h1, f2), resultSigma = vAPP(h1, f2, h1, f1), cons = [ (f1 != f2), ] } > [ FAIL ] hol_03 >Running hol_04_01... [ OK ] vAPP(srt > srt,srt,h(srt > srt,srt),c1(srt > srt)): srt > [ OK ] hol_04_01 >Running hol_04_02... [ FAIL ] vAPP(srt > srt,srt,h(srt > srt,srt),c2(srt > srt)): srt >tree: S0 -> vAPP(S2,srt,h(S3,srt),c1(S4)) ; S1 -> srt ; S2 -> [ > | srt > srt ; S3 -> srt > srt ; S4 -> srt > srt > | srt ; S4 -> srt ; S3 -> srt > ] >query: vAPP(srt > srt,srt,h(srt > srt,srt),c2(srt > srt)): srt >is: > { querySigma = vAPP(h(c2(Condition in file /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024/Kernel/Term.hpp, line 525 violated: >(unsigned)n < _arity >----- stack dump ----- >Version : Vampire 4.9 (commit ) >call stack: 0x485b85 0x78b551e3a229 0x78b551e3a16e 0x485369 0xed0b80 0xed04ab 0xece69d 0x49fdad 0x4d211d 0x498ac4 0x48e521 0x48e521 0x48e5e6 0x48ab5e 0x773613 0x7774e6 >invoking addr2line(1) ... >_start >??:? >?? >??:0 >?? >??:0 >main >??:? >Test::TestUnit::run(std::ostream&) >??:? >Test::TestUnit::runTestsWithNameSubstring(std::__cxx11::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > const&, std::ostream&) >??:? >Test::TestUnit::spawnTest(void (*)()) >??:? >__testFn__UnificationWithAbstraction__hol_04_02() >??:? >IndexTest::run() >??:? >checkTermMatches(Indexing::TermSubstitutionTree<Indexing::TermWithoutValue>&, Shell::Options::UnificationWithAbstraction, bool, Kernel::TypedTermList, Lib::Stack<UnificationResultSpec<Kernel::TermList> >) >??:? >Test::PrettyPrinter<Kernel::TermList>::operator()(std::ostream&, Kernel::TermList const&) [clone .isra.0] >tUnificationWithAbstraction.cpp:? >Test::PrettyPrinter<Kernel::TermList>::operator()(std::ostream&, Kernel::TermList const&) [clone .isra.0] >tUnificationWithAbstraction.cpp:? >Test::PrettyPrinter<Kernel::TermList>::operator()(std::ostream&, Kernel::TermList const&) [clone .isra.0] >tUnificationWithAbstraction.cpp:? >Kernel::Term::nthArgument(int) const [clone .part.0] >tUnificationWithAbstraction.cpp:? >Debug::Assertion::violated(char const*, int, char const*) >??:? >Debug::Tracer::printStack(std::ostream&) >??:? >----- end of stack dump ----- > [ FAIL ] hol_04_02 >Running hol_05_01... [ OK ] vAPP(srt > srt,srt,h(srt > srt,srt),c1(srt > srt)): srt > [ OK ] hol_05_01 >Running hol_05_02... [ FAIL ] vAPP(srt > srt,srt,h(srt > srt,srt),c2(srt > srt)): srt >tree: S0 -> vAPP(S2,srt,h(S3,srt),S4) ; S1 -> srt ; S2 -> [ > | srt > srt ; S3 -> srt > srt ; S4 -> c1(srt > srt) > | srt ; S4 -> c2(srt) ; S3 -> srt > ] >query: vAPP(srt > srt,srt,h(srt > srt,srt),c2(srt > srt)): srt >is: > { querySigma = vAPP(h(c2(Condition in file /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024/Kernel/Term.hpp, line 525 violated: >(unsigned)n < _arity >----- stack dump ----- >Version : Vampire 4.9 (commit ) >call stack: 0x485b85 0x78b551e3a229 0x78b551e3a16e 0x485369 0xed0b80 0xed04ab 0xece69d 0x4a093d 0x4d211d 0x498ac4 0x48e521 0x48e521 0x48e5e6 0x48ab5e 0x773613 0x7774e6 >invoking addr2line(1) ... >_start >??:? >?? >??:0 >?? >??:0 >main >??:? >Test::TestUnit::run(std::ostream&) >??:? >Test::TestUnit::runTestsWithNameSubstring(std::__cxx11::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > const&, std::ostream&) >??:? >Test::TestUnit::spawnTest(void (*)()) >??:? >__testFn__UnificationWithAbstraction__hol_05_02() >??:? >IndexTest::run() >??:? >checkTermMatches(Indexing::TermSubstitutionTree<Indexing::TermWithoutValue>&, Shell::Options::UnificationWithAbstraction, bool, Kernel::TypedTermList, Lib::Stack<UnificationResultSpec<Kernel::TermList> >) >??:? >Test::PrettyPrinter<Kernel::TermList>::operator()(std::ostream&, Kernel::TermList const&) [clone .isra.0] >tUnificationWithAbstraction.cpp:? >Test::PrettyPrinter<Kernel::TermList>::operator()(std::ostream&, Kernel::TermList const&) [clone .isra.0] >tUnificationWithAbstraction.cpp:? >Test::PrettyPrinter<Kernel::TermList>::operator()(std::ostream&, Kernel::TermList const&) [clone .isra.0] >tUnificationWithAbstraction.cpp:? >Kernel::Term::nthArgument(int) const [clone .part.0] >tUnificationWithAbstraction.cpp:? >Debug::Assertion::violated(char const*, int, char const*) >??:? >Debug::Tracer::printStack(std::ostream&) >??:? >----- end of stack dump ----- > [ FAIL ] hol_05_02 >Running hol_06... [ FAIL ] vAPP($o,'A',f,a): 'A' >tree: S0 -> [ > | vAPP($o,'A',f,S2) ; S1 -> 'A' ; S2 -> [ > | a > | b > ] > | a ; S1 -> $o > | b ; S1 -> $o > ] >query: vAPP($o,'A',f,a): 'A' >is: > { querySigma = vAPP(Condition in file /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024/Kernel/Term.hpp, line 525 violated: >(unsigned)n < _arity >----- stack dump ----- >Version : Vampire 4.9 (commit ) >call stack: 0x485b85 0x78b551e3a229 0x78b551e3a16e 0x485369 0xed0b80 0xed04ab 0xece69d 0x4a0e9b 0x4d211d 0x498ac4 0x48e521 0x48e77c 0x48ab5e 0x773613 0x7774e6 >invoking addr2line(1) ... >_start >??:? >?? >??:0 >?? >??:0 >main >??:? >Test::TestUnit::run(std::ostream&) >??:? >Test::TestUnit::runTestsWithNameSubstring(std::__cxx11::basic_string<char, std::char_traits<char>, Lib::STLAllocator<char> > const&, std::ostream&) >??:? >Test::TestUnit::spawnTest(void (*)()) >??:? >__testFn__UnificationWithAbstraction__hol_06() >??:? >IndexTest::run() >??:? >checkTermMatches(Indexing::TermSubstitutionTree<Indexing::TermWithoutValue>&, Shell::Options::UnificationWithAbstraction, bool, Kernel::TypedTermList, Lib::Stack<UnificationResultSpec<Kernel::TermList> >) >??:? >Test::PrettyPrinter<Kernel::TermList>::operator()(std::ostream&, Kernel::TermList const&) [clone .isra.0] >tUnificationWithAbstraction.cpp:? >Test::printOp(std::ostream&, Kernel::Term const*, char const*) [clone .isra.0] >tUnificationWithAbstraction.cpp:? >Kernel::Term::nthArgument(int) const [clone .part.0] >tUnificationWithAbstraction.cpp:? >Debug::Assertion::violated(char const*, int, char const*) >??:? >Debug::Tracer::printStack(std::ostream&) >??:? >----- end of stack dump ----- > [ FAIL ] 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... [ FAIL ] vAPP(srt > srt,srt,f,b): srt >tree: S0 -> vAPP(srt > srt,srt,f,a) ; S1 -> srt >query: vAPP(srt > srt,srt,f,b): srt >is: > { querySigma = vAPP(f, c, f, b), resultSigma = vAPP(f, c, f, a), cons = [ ] } >expected: > { querySigma = vAPP(f, c, f, b), resultSigma = vAPP(f, c, f, a), cons = [ (a != b), ] } > [ FAIL ] 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 44 (84.6) % > - fail 8 (15.4) % ><end of output> >Test time = 0.12 sec >---------------------------------------------------------- >Test Failed. >"UnificationWithAbstraction" end time: Sep 30 20:32 CEST >"UnificationWithAbstraction" time elapsed: 00:00:00 >---------------------------------------------------------- > >12/39 Testing: Induction >12/39 Test: Induction >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Induction" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Induction" start time: Sep 30 20:32 CEST >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 = 0.12 sec >---------------------------------------------------------- >Test Passed. >"Induction" end time: Sep 30 20:32 CEST >"Induction" time elapsed: 00:00:00 >---------------------------------------------------------- > >7/39 Testing: ArithmeticSubtermGeneralization >7/39 Test: ArithmeticSubtermGeneralization >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "ArithmeticSubtermGeneralization" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"ArithmeticSubtermGeneralization" start time: Sep 30 20:32 CEST >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 = 0.17 sec >---------------------------------------------------------- >Test Passed. >"ArithmeticSubtermGeneralization" end time: Sep 30 20:32 CEST >"ArithmeticSubtermGeneralization" time elapsed: 00:00:00 >---------------------------------------------------------- > >8/39 Testing: InterpretedFunctions >8/39 Test: InterpretedFunctions >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "InterpretedFunctions" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"InterpretedFunctions" start time: Sep 30 20:32 CEST >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 = 0.27 sec >---------------------------------------------------------- >Test Passed. >"InterpretedFunctions" end time: Sep 30 20:32 CEST >"InterpretedFunctions" time elapsed: 00:00:00 >---------------------------------------------------------- > >39/39 Testing: Z3Interfacing >39/39 Test: Z3Interfacing >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "Z3Interfacing" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"Z3Interfacing" start time: Sep 30 20:32 CEST >Output: >---------------------------------------------------------- >Running solve__real__simple_01... [Z3] add (naming): (= v1 (= 0.0 3.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 (= (+ 3.0 (* 2.0 7.0)) 17.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 (= false true)) >[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 zero nil) (cons (succEven (succOdd 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 zero nil) (cons (succEven (succOdd 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 3.0 nil) (cons cc nil))) >[Z3] solve result: sat > [ OK ] instantiate__list_01 >Running instantiate__list_02... [Z3] add (naming): (= v1 (= (cons 2.0 nil) (|'cons@1'_$| cl))) >[Z3] add (naming): (= v2 (= 1.0 (|'cons@0'_$| cl))) >[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 = 0.29 sec >---------------------------------------------------------- >Test Passed. >"Z3Interfacing" end time: Sep 30 20:32 CEST >"Z3Interfacing" time elapsed: 00:00:00 >---------------------------------------------------------- > >38/39 Testing: TheoryInstAndSimp >38/39 Test: TheoryInstAndSimp >Command: "/var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build/vtest" "run" "TheoryInstAndSimp" >Directory: /var/tmp/portage/sci-mathematics/vampire-4.9/work/vampire-4.9casc2024_build >"TheoryInstAndSimp" start time: Sep 30 20:32 CEST >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... [ OK ] generalisation_1 >Running generalisation_2... [ OK ] generalisation_2 >Running generalisation_3... [ OK ] generalisation_3 >Running generalisation_4... [ OK ] generalisation_4 >Running generalisation_5... [ OK ] generalisation_5 > >Tests run: 26 > - ok 26 (100.0) % > - fail 0 (0.0) % ><end of output> >Test time = 0.73 sec >---------------------------------------------------------- >Test Passed. >"TheoryInstAndSimp" end time: Sep 30 20:32 CEST >"TheoryInstAndSimp" time elapsed: 00:00:00 >---------------------------------------------------------- > >End testing: Sep 30 20:32 CEST
<b>You cannot view the attachment while viewing its details because your browser does not support IFRAMEs. <a href="attachment.cgi?id=904423">View the attachment on a separate page</a>.</b>
View Attachment As Raw
Actions:
View
Attachments on
bug 940574
:
904422
| 904423
