Last active
December 13, 2016 09:32
-
-
Save nekketsuuu/44f492498f09567af752466a6211dbce to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| dotnet$ xbuild Microsoft.Z3.csproj | |
| XBuild Engine Version 12.0 | |
| Mono, Version 4.2.1.0 | |
| Copyright (C) 2005-2013 Various Mono authors | |
| Build started 2016/12/13 11:30:40. | |
| __________________________________________________ | |
| Project "/home/nek/bitbucket/spacer/code/src/api/dotnet/Microsoft.Z3.csproj" (default target(s)): | |
| Target PrepareForBuild: | |
| Configuration: Debug Platform: AnyCPU | |
| Created directory "../Debug/" | |
| Created directory "obj/Debug/" | |
| Target GenerateSatelliteAssemblies: | |
| No input files were specified for target GenerateSatelliteAssemblies, skipping. | |
| Target CoreCompile: | |
| Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /delaysign- /debug+ /optimize- /out:obj/Debug/Microsoft.Z3.dll AlgebraicNum.cs ApplyResult.cs ArithExpr.cs ArithSort.cs ArrayExpr.cs ArraySort.cs AST.cs ASTMap.cs ASTVector.cs BitVecExpr.cs BitVecNum.cs BitVecSort.cs BoolExpr.cs BoolSort.cs Constructor.cs ConstructorList.cs DatatypeExpr.cs DatatypeSort.cs FPExpr.cs FPNum.cs FPRMExpr.cs FPRMNum.cs FPRMSort.cs FPSort.cs Global.cs IDecRefQueue.cs Enumerations.cs EnumSort.cs Expr.cs FiniteDomainSort.cs Fixedpoint.cs FuncDecl.cs FuncInterp.cs Goal.cs InterpolationContext.cs IntExpr.cs IntNum.cs IntSort.cs IntSymbol.cs ListSort.cs Model.cs Optimize.cs Params.cs ParamDescrs.cs Pattern.cs RatNum.cs RealExpr.cs RealSort.cs RelationSort.cs SetSort.cs Statistics.cs Status.cs Context.cs Probe.cs Solver.cs StringSymbol.cs Tactic.cs TupleSort.cs UninterpretedSort.cs Z3Exception.cs Log.cs Native.cs Properties/AssemblyInfo.cs Quantifier.cs Sort.cs Symbol.cs Version.cs Z3Object.cs obj/Debug/.NETFramework,Version=v4.0,Profile=Client.AssemblyAttribute.cs /target:library /unsafe+ /define:"DEBUG;TRACE" /doc:../Debug/Microsoft.Z3.XML /nostdlib /reference:/usr/lib/mono/gac/System/4.0.0.0__b77a5c561934e089/System.dll /reference:/usr/lib/mono/gac/System.Numerics/4.0.0.0__b77a5c561934e089/System.Numerics.dll /reference:/usr/lib/mono/gac/System.Core/4.0.0.0__b77a5c561934e089/System.Core.dll /warn:4 | |
| CSC: error CS0518: The predefined type `System.Object' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.ValueType' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Attribute' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Int32' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.UInt32' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Int64' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.UInt64' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Single' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Double' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Char' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Int16' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Decimal' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Boolean' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.SByte' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Byte' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.UInt16' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.String' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Enum' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Delegate' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.MulticastDelegate' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Void' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Array' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Type' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Collections.IEnumerator' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Collections.IEnumerable' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.IDisposable' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.IntPtr' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.UIntPtr' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.RuntimeFieldHandle' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.RuntimeTypeHandle' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Exception' is not defined or imported | |
| Task "Csc" execution -- FAILED | |
| Done building target "CoreCompile" in project "/home/nek/bitbucket/spacer/code/src/api/dotnet/Microsoft.Z3.csproj".-- FAILED | |
| Done building project "/home/nek/bitbucket/spacer/code/src/api/dotnet/Microsoft.Z3.csproj".-- FAILED | |
| Build FAILED. | |
| Errors: | |
| /home/nek/bitbucket/spacer/code/src/api/dotnet/Microsoft.Z3.csproj (default targets) -> | |
| /usr/lib/mono/4.5/Microsoft.CSharp.targets (CoreCompile target) -> | |
| CSC: error CS0518: The predefined type `System.Object' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.ValueType' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Attribute' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Int32' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.UInt32' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Int64' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.UInt64' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Single' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Double' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Char' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Int16' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Decimal' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Boolean' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.SByte' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Byte' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.UInt16' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.String' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Enum' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Delegate' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.MulticastDelegate' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Void' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Array' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Type' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Collections.IEnumerator' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Collections.IEnumerable' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.IDisposable' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.IntPtr' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.UIntPtr' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.RuntimeFieldHandle' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.RuntimeTypeHandle' is not defined or imported | |
| CSC: error CS0518: The predefined type `System.Exception' is not defined or imported | |
| 0 Warning(s) | |
| 31 Error(s) | |
| Time Elapsed 00:00:01.0573810 | |
| dotnet$ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| dotnet$ xbuild Microsoft.Z3.csproj | |
| XBuild Engine Version 14.0 | |
| Mono, Version 4.6.2.0 | |
| Copyright (C) 2005-2013 Various Mono authors | |
| Build started 2016/12/13 12:57:44. | |
| __________________________________________________ | |
| Project "/home/nek/bitbucket/spacer/code/src/api/dotnet/Microsoft.Z3.csproj" (default target(s)): | |
| Target PrepareForBuild: | |
| Configuration: Debug Platform: AnyCPU | |
| Target GenerateSatelliteAssemblies: | |
| No input files were specified for target GenerateSatelliteAssemblies, skipping. | |
| Target _GenerateTargetFrameworkMonikerAttribute: | |
| Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. | |
| Target CoreCompile: | |
| Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /delaysign- /debug+ /optimize- /out:obj/Debug/Microsoft.Z3.dll AlgebraicNum.cs ApplyResult.cs ArithExpr.cs ArithSort.cs ArrayExpr.cs ArraySort.cs AST.cs ASTMap.cs ASTVector.cs BitVecExpr.cs BitVecNum.cs BitVecSort.cs BoolExpr.cs BoolSort.cs Constructor.cs ConstructorList.cs DatatypeExpr.cs DatatypeSort.cs FPExpr.cs FPNum.cs FPRMExpr.cs FPRMNum.cs FPRMSort.cs FPSort.cs Global.cs IDecRefQueue.cs Enumerations.cs EnumSort.cs Expr.cs FiniteDomainSort.cs Fixedpoint.cs FuncDecl.cs FuncInterp.cs Goal.cs InterpolationContext.cs IntExpr.cs IntNum.cs IntSort.cs IntSymbol.cs ListSort.cs Model.cs Optimize.cs Params.cs ParamDescrs.cs Pattern.cs RatNum.cs RealExpr.cs RealSort.cs RelationSort.cs SetSort.cs Statistics.cs Status.cs Context.cs Probe.cs Solver.cs StringSymbol.cs Tactic.cs TupleSort.cs UninterpretedSort.cs Z3Exception.cs Log.cs Native.cs Properties/AssemblyInfo.cs Quantifier.cs Sort.cs Symbol.cs Version.cs Z3Object.cs obj/Debug/.NETFramework,Version=v4.0,Profile=Client.AssemblyAttribute.cs /target:library /unsafe+ /define:"DEBUG;TRACE" /doc:../Debug/Microsoft.Z3.XML /nostdlib /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Numerics.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 | |
| InterpolationContext.cs(28,16): warning CS1574: XML comment on `Microsoft.Z3.InterpolationContext.InterpolationContext(System.Collections.Generic.Dictionary<string,string>)' has cref attribute `Context.Context(Dictionary<string, string>)' that could not be resolved | |
| Target DeployOutputFiles: | |
| Copying file from '/home/nek/bitbucket/spacer/code/src/api/dotnet/obj/Debug/Microsoft.Z3.dll.mdb' to '/home/nek/bitbucket/spacer/code/src/api/Debug/Microsoft.Z3.dll.mdb' | |
| Copying file from '/home/nek/bitbucket/spacer/code/src/api/dotnet/obj/Debug/Microsoft.Z3.dll' to '/home/nek/bitbucket/spacer/code/src/api/Debug/Microsoft.Z3.dll' | |
| Done building project "/home/nek/bitbucket/spacer/code/src/api/dotnet/Microsoft.Z3.csproj". | |
| Build succeeded. | |
| Warnings: | |
| /home/nek/bitbucket/spacer/code/src/api/dotnet/Microsoft.Z3.csproj (default targets) -> | |
| /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> | |
| InterpolationContext.cs(28,16): warning CS1574: XML comment on `Microsoft.Z3.InterpolationContext.InterpolationContext(System.Collections.Generic.Dictionary<string,string>)' has cref attribute `Context.Context(Dictionary<string, string>)' that could not be resolved | |
| 1 Warning(s) | |
| 0 Error(s) | |
| Time Elapsed 00:00:00.5530750 | |
| dotnet$ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| T2/src$ xbuild | |
| XBuild Engine Version 14.0 | |
| Mono, Version 4.6.2.0 | |
| Copyright (C) 2005-2013 Various Mono authors | |
| Build started 2016/12/13 13:05:33. | |
| __________________________________________________ | |
| Project "/home/nek/github/T2/src/T2.sln" (default target(s)): | |
| Target ValidateSolutionConfiguration: | |
| Building solution configuration "Debug|x86". | |
| Target Build: | |
| Project "/home/nek/github/T2/src/T2-Library.fsproj" (default target(s)): | |
| Target PrepareForBuild: | |
| Configuration: Debug Platform: x86 | |
| Created directory "bin/Debug/" | |
| Created directory "obj/x86/Debug/" | |
| Target CopyFilesMarkedCopyLocal: | |
| Copying file from '/home/nek/github/T2/src/packages/FsLexYacc.Runtime.6.1.0/lib/net40/FsLexYacc.Runtime.dll' to '/home/nek/github/T2/src/bin/Debug/FsLexYacc.Runtime.dll' | |
| Copying file from '/usr/lib/mono/gac/FSharp.Core/4.3.1.0__b03f5f7f11d50a3a/FSharp.Core.dll' to '/home/nek/github/T2/src/bin/Debug/FSharp.Core.dll' | |
| Copying file from '/home/nek/github/T2/src/Microsoft.Z3.dll' to '/home/nek/github/T2/src/bin/Debug/Microsoft.Z3.dll' | |
| Target GenerateSatelliteAssemblies: | |
| No input files were specified for target GenerateSatelliteAssemblies, skipping. | |
| Target CallFsLex: | |
| Tool /home/nek/github/T2/src/packages/FsLexYacc.6.1.0/build/fslex.exe execution started with arguments: -o absflex.fs absflex.fsl | |
| compiling to dfas (can take a while...) | |
| 133 states | |
| writing output | |
| Target CallFsYacc: | |
| Tool /home/nek/github/T2/src/packages/FsLexYacc.6.1.0/build/fsyacc.exe execution started with arguments: -o absparse.fs --module Microsoft.Research.T2.Absparse absparse.fsy | |
| building tables | |
| computing first function...time: 00:00:00.0229433 | |
| building kernels...time: 00:00:00.0169750 | |
| building kernel table...time: 00:00:00.0049784 | |
| computing lookahead relations...........................................................................................................................................................................................................................................time: 00:00:00.0251779 | |
| building lookahead table...time: 00:00:00.0051796 | |
| building action table...state 119: shift/reduce error on AND_OP | |
| state 119: shift/reduce error on OR_OP | |
| state 194: shift/reduce error on AND_OP | |
| state 194: shift/reduce error on OR_OP | |
| time: 00:00:00.0197722 | |
| building goto table...time: 00:00:00.0052569 | |
| returning tables. | |
| 4 shift/reduce conflicts | |
| 232 states | |
| 23 nonterminals | |
| 51 terminals | |
| 80 productions | |
| #rows in action table: 232 | |
| Target CoreCompile: | |
| Tool /usr/lib/cli/fsharp/fsc.exe execution started with arguments: -o:obj/x86/Debug/Microsoft.Research.T2.dll -g --debug:full --noframework --define:DEBUG --define:TRACE --doc:bin/Debug/Microsoft.Research.T2.XML --optimize- --tailcalls- --platform:x86 -r:packages/FsLexYacc.Runtime.6.1.0/lib/net40/FsLexYacc.Runtime.dll -r:/usr/lib/mono/4.5-api/mscorlib.dll -r:/usr/lib/mono/gac/FSharp.Core/4.3.1.0__b03f5f7f11d50a3a/FSharp.Core.dll -r:Microsoft.Z3.dll -r:/usr/lib/mono/4.5-api/System.dll -r:/usr/lib/mono/4.5-api/System.Numerics.dll -r:/usr/lib/mono/4.5-api/System.Core.dll --target:library --warn:3 --warnaserror:76 --fullpaths --flaterrors --highentropyva- utils.fs parameters.fs log.fs stats.fs test.fs scc.fs dominators.fs gensym.fs z.fs var.fs term.fs formula.fs parseError.fs sparselinear.fs relation.fs interpolantSequence.fs interpolantSingle.fs programs.fs symex.fs Output.fs IIntAbsDom.fs octagon2.fs IntervalIntDom.fs counterexample.fs analysis.fs PriorityQueue.fs SafetyInterface.fs Impact.fs MuZ.fs Safety.fs rankfunction.fs ctl.fs instrumentation.fs lasso.fs recurrentsets.fs termination.fs absparse.fs absflex.fs ctl_parser.fs input.fs | |
| F# Compiler for F# 4.0 (Open Source Edition) | |
| Freely distributed under the Apache 2.0 Open Source License | |
| /home/nek/github/T2/src/symex.fs(224,64): warning FS0044: This construct is deprecated. please use List.item | |
| /home/nek/github/T2/src/termination.fs(1336,15): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'U (_, _)' may indicate a case not covered by the pattern(s). | |
| /home/nek/github/T2/src/termination.fs(1350,42): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'W (_, _)' may indicate a case not covered by the pattern(s). | |
| /home/nek/github/T2/src/termination.fs(1367,31): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'U (_, _)' may indicate a case not covered by the pattern(s). | |
| /home/nek/github/T2/src/termination.fs(1385,46): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'U (_, _)' may indicate a case not covered by the pattern(s). | |
| Target DeployOutputFiles: | |
| Copying file from '/home/nek/github/T2/src/obj/x86/Debug/Microsoft.Research.T2.dll.mdb' to '/home/nek/github/T2/src/bin/Debug/Microsoft.Research.T2.dll.mdb' | |
| Copying file from '/home/nek/github/T2/src/obj/x86/Debug/Microsoft.Research.T2.dll' to '/home/nek/github/T2/src/bin/Debug/Microsoft.Research.T2.dll' | |
| Target AfterBuild: | |
| Copying file from '/home/nek/github/T2/src/libz3.so' to '/home/nek/github/T2/src/bin/Debug/libz3.so' | |
| Done building project "/home/nek/github/T2/src/T2-Library.fsproj". | |
| Project "/home/nek/github/T2/Mono.Options/Mono.Options.csproj" (default target(s)): | |
| Target PrepareForBuild: | |
| Configuration: Debug Platform: x86 | |
| Created directory "bin/Debug/" | |
| Created directory "obj/x86/Debug/" | |
| Target GenerateSatelliteAssemblies: | |
| No input files were specified for target GenerateSatelliteAssemblies, skipping. | |
| Target CoreCompile: | |
| Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug+ /optimize- /out:obj/x86/Debug/Mono.Options.dll Options.cs Properties/AssemblyInfo.cs obj/x86/Debug/.NETFramework,Version=v4.5.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:x86 /reference:/usr/lib/mono/4.5-api/System.dll /reference:/usr/lib/mono/4.5-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.5-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.5-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.5-api/System.Data.dll /reference:/usr/lib/mono/4.5-api/System.Xml.dll /reference:/usr/lib/mono/4.5-api/System.Core.dll /reference:/usr/lib/mono/4.5-api//mscorlib.dll /warn:4 | |
| Target DeployOutputFiles: | |
| Copying file from '/home/nek/github/T2/Mono.Options/obj/x86/Debug/Mono.Options.dll.mdb' to '/home/nek/github/T2/Mono.Options/bin/Debug/Mono.Options.dll.mdb' | |
| Copying file from '/home/nek/github/T2/Mono.Options/obj/x86/Debug/Mono.Options.dll' to '/home/nek/github/T2/Mono.Options/bin/Debug/Mono.Options.dll' | |
| Done building project "/home/nek/github/T2/Mono.Options/Mono.Options.csproj". | |
| Project "/home/nek/github/T2/src/T2-CLI.fsproj" (default target(s)): | |
| Target PrepareForBuild: | |
| Configuration: Debug Platform: x86 | |
| Target CopyFilesMarkedCopyLocal: | |
| Copying file from '/home/nek/github/T2/Mono.Options/bin/Debug/Mono.Options.dll' to '/home/nek/github/T2/src/bin/Debug/Mono.Options.dll' | |
| Copying file from '/home/nek/github/T2/Mono.Options/bin/Debug/Mono.Options.dll.mdb' to '/home/nek/github/T2/src/bin/Debug/Mono.Options.dll.mdb' | |
| Target GenerateSatelliteAssemblies: | |
| No input files were specified for target GenerateSatelliteAssemblies, skipping. | |
| Target CoreCompile: | |
| Tool /usr/lib/cli/fsharp/fsc.exe execution started with arguments: -o:obj/x86/Debug/T2.exe -g --noframework --define:DEBUG --optimize- --tailcalls- --platform:x86 -r:/usr/lib/mono/gac/FSharp.Core/4.3.1.0__b03f5f7f11d50a3a/FSharp.Core.dll -r:packages/FsLexYacc.Runtime.6.1.0/lib/net40/FsLexYacc.Runtime.dll -r:/usr/lib/mono/4.5-api/mscorlib.dll -r:/usr/lib/mono/4.5-api/System.dll -r:/usr/lib/mono/4.5-api/System.Numerics.dll -r:Microsoft.Z3.dll -r:/usr/lib/mono/4.5-api/System.Core.dll -r:/home/nek/github/T2/Mono.Options/bin/Debug//Mono.Options.dll -r:/home/nek/github/T2/src/bin/Debug//Microsoft.Research.T2.dll --target:exe --nowarn:62 --warn:3 --warnaserror:76 --fullpaths --flaterrors --highentropyva- arguments.fs programTests.fs main.fs | |
| F# Compiler for F# 4.0 (Open Source Edition) | |
| Freely distributedeployOutputFiles: | |
| Copying file from '/home/nek/github/T2/src/obj/x86/Debug/T2.exe.mdb' to '/home/nek/github/T2/src/bin/Debug/T2.exe.mdb' | |
| Copying file from '/home/nek/github/T2/src/obj/x86/Debug/T2.exe' to '/home/nek/github/T2/src/bin/Debug/T2.exe' | |
| Target AfterBuild: | |
| Copying file from '/home/nek/github/T2/src/libz3.so' to '/home/nek/github/T2/src/bin/Debug/libz3.so' | |
| Done building project "/home/nek/github/T2/src/T2-CLI.fsproj". | |
| Done building project "/home/nek/github/T2/src/T2.sln". | |
| Build succeeded. | |
| Warnings: | |
| /home/nek/github/T2/src/T2.sln (default targets) -> | |
| (Build target) -> | |
| /home/nek/github/T2/src/T2-Library.fsproj (default targets) -> | |
| /usr/lib/mono/4.5/Microsoft.FSharp.Targets (CoreCompile target) -> | |
| /home/nek/github/T2/src/symex.fs(224,64): warning FS0044: This construct is deprecated. please use List.item | |
| /home/nek/github/T2/src/termination.fs(1336,15): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'U (_, _)' may indicate a case not covered by the pattern(s). | |
| /home/nek/github/T2/src/termination.fs(1350,42): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'W (_, _)' may indicate a case not covered by the pattern(s). | |
| /home/nek/github/T2/src/termination.fs(1367,31): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'U (_, _)' may indicate a case not covered by the pattern(s). | |
| /home/nek/github/T2/src/termination.fs(1385,46): warning FS0025: Incomplete pattern matches on this expression. For example, the value 'U (_, _)' may indicate a case not covered by the pattern(s). | |
| 5 Warning(s) | |
| 0 Error(s) | |
| Time Elapsed 00:00:11.0017340 | |
| T2/src$ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| T2/test$ mono ../src/bin/Release/T2.exe --tests | |
| Running tests-------------------------------------------- | |
| Using timeout of 300.00 s | |
| Termination test testsuite/small01.t2: OK after 00:00:00.2615640 | |
| Safety test testsuite/small02.t2 [loc 10000]: OK after 00:00:00.0052610 | |
| Safety test testsuite/small03.t2 [loc 10000]: OK after 00:00:00.0041490 | |
| Safety test testsuite/small04.t2 [loc 10000]: OK after 00:00:00.0041060 | |
| Safety test testsuite/small05.t2 [loc 10000]: OK after 00:00:00.0040460 | |
| Safety test testsuite/small06.t2 [loc 10000]: OK after 00:00:00.0065610 | |
| Safety test testsuite/small07.t2 [loc 10000]: OK after 00:00:00.0113230 | |
| Safety test testsuite/small08.t2 [loc 10000]: OK after 00:00:00.0220110 | |
| Safety test testsuite/small09.t2 [loc 10000]: OK after 00:00:00.0243530 | |
| Termination test testsuite/small12.t2: OK after 00:00:00.0116780 | |
| Termination test testsuite/small13.t2: OK after 00:00:00.0156800 | |
| Safety test testsuite/small14.t2 [loc 10000]: OK after 00:00:00.0133070 | |
| Termination test testsuite/small19.t2: OK after 00:00:00.0135930 | |
| Termination test testsuite/small20.t2: OK after 00:00:00.0248700 | |
| Termination test testsuite/small21.t2: OK after 00:00:00.0203560 | |
| Safety test testsuite/small24.t2 [loc 10000]: OK after 00:00:00.0007180 | |
| Safety test testsuite/small25.t2 [loc 10000]: Stacktrace: | |
| at <unknown> <0xffffffff> | |
| at (wrapper managed-to-native) Microsoft.Z3.Native/LIB.Z3_fixedpoint_query (intptr,intptr,intptr) <0x0006b> | |
| at Microsoft.Z3.Native.Z3_fixedpoint_query (intptr,intptr,intptr) <0x0001f> | |
| at Microsoft.Z3.Fixedpoint.Query (Microsoft.Z3.BoolExpr) <0x0006b> | |
| at Microsoft.Research.T2.MuZ/MuZWrapper.CallSpacer (System.Collections.Generic.Dictionary`2<int, Microsoft.Z3.FuncDecl>,Microsoft.FSharp.Collections.FSharpList`1<System.Tuple`2<Microsoft.Z3.Quantifier, Microsoft.Z3.StringSymbol>>,Microsoft.Z3.BoolExpr) <0x003df> | |
| at Microsoft.Research.T2.MuZ/MuZWrapper.Microsoft-Research-T2-SafetyInterface-SafetyProver-ErrorLocationReachable () <0x00267> | |
| at Microsoft.Research.T2.Safety.prover (Microsoft.Research.T2.Parameters/parameters,Microsoft.Research.T2.Programs/Program,int) <0x0007e> | |
| at Microsoft.Research.T2.ProgramTests/safety_prover@102.Invoke (Microsoft.Research.T2.Programs/Program,int) <0x00027> | |
| at Microsoft.FSharp.Core.FSharpFunc`2<Microsoft.Research.T2.Programs/Program, int>.InvokeFast<bool> (Microsoft.FSharp.Core.FSharpFunc`2<Microsoft.Research.T2.Programs/Program, Microsoft.FSharp.Core.FSharpFunc`2<int, bool>>,Microsoft.Research.T2.Programs/Program,int) <0x00074> | |
| at Microsoft.Research.T2.ProgramTests/register_tests@176-16.Invoke (Microsoft.FSharp.Core.Unit) <0x00023> | |
| at Microsoft.Research.T2.Test/run_test@71-1<bool>.Invoke (System.Tuple`3<bool, Microsoft.FSharp.Core.FSharpFunc`2<Microsoft.FSharp.Core.Unit, bool>, string>) <0x0017e> | |
| at Microsoft.FSharp.Primitives.Basics.List.iter<T_REF> (Microsoft.FSharp.Core.FSharpFunc`2<T_REF, Microsoft.FSharp.Core.Unit>,Microsoft.FSharp.Collections.FSharpList`1<T_REF>) <0x00047> | |
| at Microsoft.FSharp.Collections.ListModule.Iterate<T_REF> (Microsoft.FSharp.Core.FSharpFunc`2<T_REF, Microsoft.FSharp.Core.Unit>,Microsoft.FSharp.Collections.FSharpList`1<T_REF>) <0x0002f> | |
| at Microsoft.Research.T2.Test.run_tests (double) <0x0024f> | |
| at Microsoft.Research.T2.Main.main (string[]) <0x0028b> | |
| at (wrapper runtime-invoke) <Module>.runtime_invoke_int_object (object,intptr,intptr,intptr) <0x000f5> | |
| Native stacktrace: | |
| mono() [0x4accca] | |
| mono() [0x5040fe] | |
| mono() [0x4275d7] | |
| /lib/x86_64-linux-gnu/libpthread.so.0(+0x11390) [0x7f4520b10390] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0xdc1c33) [0x7f451cec5c33] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0x3ae4df) [0x7f451c4b24df] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0x3aec53) [0x7f451c4b2c53] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0x3aedf9) [0x7f451c4b2df9] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0x3b29a9) [0x7f451c4b69a9] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0x3b3463) [0x7f451c4b7463] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0x41afc8) [0x7f451c51efc8] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0x3efef6) [0x7f451c4f3ef6] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(+0x1dfe36) [0x7f451c2e3e36] | |
| /home/nek/github/T2/src/bin/Release/libz3.so(Z3_fixedpoint_query+0xb3) [0x7f451c18acd3] | |
| [0x405bb0ec] | |
| Debug info from gdb: | |
| Could not attach to process. If your uid matches the uid of the target | |
| process, check the setting of /proc/sys/kernel/yama/ptrace_scope, or try | |
| again as the root user. For more details, see /etc/sysctl.d/10-ptrace.conf | |
| ptrace: Operation not permitted. | |
| No threads. | |
| ================================================================= | |
| Got a SIGSEGV while executing native code. This usually indicates | |
| a fatal error in the mono runtime or one of the native libraries | |
| used by your application. | |
| ================================================================= | |
| Aborted (core dumped) | |
| T2/test$ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment