今日の取り組み
js-symbolic-execution導入続き
機能に引き続き再びチャレンジ！今日はよく寝たし、うまく行くはず...!
maru@marU:/mnt/sharefolder/js-symbolic-executor/js-symbolic-executor$ ant
Buildfile: /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build.xml
init:
closure-compiler:
compile:
[javac] /mnt/sharefolder/js-symbolic-executor/closure-compiler/build.xml:54: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
[javac] /mnt/sharefolder/js-symbolic-executor/closure-compiler/build.xml:60: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
jar:
check-config.status:
configure-cvc3:
cvc3:
compile:
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build.xml:69: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
[javac] Compiling 26 source files to /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build/classes
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicExpression.java:19: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:23: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:24: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Op;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:25: エラー: パッケージcvc3は存在しません
[javac] import cvc3.QueryResult;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:26: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Type;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:27: エラー: パッケージcvc3は存在しません
[javac] import cvc3.ValidityChecker;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicExpression.java:36: エラー: シンボルを見つけられません
[javac] public Expr toCvc3(Cvc3Context context);
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: インタフェース SymbolicExpression
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:45: エラー: シンボルを見つけられません
[javac] private final ValidityChecker context;
[javac] ^
[javac] シンボル: クラス ValidityChecker
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:51: エラー: シンボルを見つけられません
[javac] private final Type intType;
[javac] ^
[javac] シンボル: クラス Type
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:52: エラー: シンボルを見つけられません
[javac] private final Type stringType;
[javac] ^
[javac] シンボル: クラス Type
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:53: エラー: シンボルを見つけられません
[javac] private final Type jsType;
[javac] ^
[javac] シンボル: クラス Type
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:104: エラー: シンボルを見つけられません
[javac] public Expr construct(String constructor, Expr... args) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:104: エラー: シンボルを見つけられません
[javac] public Expr construct(String constructor, Expr... args) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:120: エラー: シンボルを見つけられません
[javac] public Expr lookupVar(String name) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:125: エラー: シンボルを見つけられません
[javac] public Op lookupOp(String opString) {
[javac] ^
[javac] シンボル: クラス Op
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:132: エラー: シンボルを見つけられません
[javac] public Expr varExpr(String name, Type type) {
[javac] ^
[javac] シンボル: クラス Type
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:132: エラー: シンボルを見つけられません
[javac] public Expr varExpr(String name, Type type) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:141: エラー: シンボルを見つけられません
[javac] public Expr funExpr(String opString, Expr... exprs) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:141: エラー: シンボルを見つけられません
[javac] public Expr funExpr(String opString, Expr... exprs) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:152: エラー: シンボルを見つけられません
[javac] public Expr funExpr(String opString, SymbolicExpression[] args) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:170: エラー: シンボルを見つけられません
[javac] private Expr toBoolean(SymbolicExpression constraint) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:205: エラー: シンボルを見つけられません
[javac] private HashMap<Expr, Expr> getConcreteModel() {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:205: エラー: シンボルを見つけられません
[javac] private HashMap<Expr, Expr> getConcreteModel() {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:210: エラー: シンボルを見つけられません
[javac] public Expr jsNum(int n) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:215: エラー: シンボルを見つけられません
[javac] public Expr ratExpr(int n){
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:230: エラー: シンボルを見つけられません
[javac] private final HashMap<String, Expr> stringConstants = Maps.newHashMap();
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:233: エラー: シンボルを見つけられません
[javac] public Expr stringConstant(String string) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:263: エラー: シンボルを見つけられません
[javac] private JsValue exprToJsValue(Expr variable, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:263: エラー: シンボルを見つけられません
[javac] private JsValue exprToJsValue(Expr variable, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:263: エラー: シンボルを見つけられません
[javac] private JsValue exprToJsValue(Expr variable, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:295: エラー: シンボルを見つけられません
[javac] private int exprToJsNum(Expr expr, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:295: エラー: シンボルを見つけられません
[javac] private int exprToJsNum(Expr expr, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:295: エラー: シンボルを見つけられません
[javac] private int exprToJsNum(Expr expr, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:317: エラー: シンボルを見つけられません
[javac] private String exprToJsString(Expr expr, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:317: エラー: シンボルを見つけられません
[javac] private String exprToJsString(Expr expr, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:317: エラー: シンボルを見つけられません
[javac] private String exprToJsString(Expr expr, Map<Expr, Expr> model) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:345: エラー: シンボルを見つけられません
[javac] private int constIntExprToInt(Expr value) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/ApiBasedInputGenerator.java:21: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsBool.java:19: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsBool.java:41: エラー: シンボルを見つけられません
[javac] public Expr toCvc3(Cvc3Context context) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス JsBool
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsDouble.java:19: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsDouble.java:41: エラー: シンボルを見つけられません
[javac] public Expr toCvc3(Cvc3Context context) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス JsDouble
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsNull.java:19: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsNull.java:36: エラー: シンボルを見つけられません
[javac] public Expr toCvc3(Cvc3Context context) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス JsNull
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsString.java:19: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsString.java:42: エラー: シンボルを見つけられません
[javac] public Expr toCvc3(Cvc3Context context) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス JsString
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsUndefined.java:19: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/JsUndefined.java:36: エラー: シンボルを見つけられません
[javac] public Expr toCvc3(Cvc3Context context) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス JsUndefined
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicOperation.java:21: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicOperation.java:53: エラー: シンボルを見つけられません
[javac] public Expr toCvc3(Cvc3Context context) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス SymbolicOperation
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicValue.java:19: エラー: パッケージcvc3は存在しません
[javac] import cvc3.Expr;
[javac] ^
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicValue.java:47: エラー: シンボルを見つけられません
[javac] public Expr toCvc3(Cvc3Context context) {
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス SymbolicValue
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:57: エラー: シンボルを見つけられません
[javac] context = ValidityChecker.create();
[javac] ^
[javac] シンボル: 変数 ValidityChecker
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:88: エラー: シンボルを見つけられません
[javac] Expr symVar = varExpr("sym" + i, jsType);
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:89: エラー: シンボルを見つけられません
[javac] Expr symInt = varExpr("symInt" + i, intType);
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:90: エラー: シンボルを見つけられません
[javac] Expr symStr = varExpr("symStr" + i, stringType);
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:153: エラー: シンボルを見つけられません
[javac] Op op = lookupOp(opString);
[javac] ^
[javac] シンボル: クラス Op
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:154: エラー: シンボルを見つけられません
[javac] List<Expr> argList = Lists.newArrayListWithCapacity(args.length);
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:184: エラー: シンボルを見つけられません
[javac] QueryResult queryResult = context.query(toBoolean(constraint));
[javac] ^
[javac] シンボル: クラス QueryResult
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:185: エラー: シンボルを見つけられません
[javac] if (queryResult == QueryResult.VALID) {
[javac] ^
[javac] シンボル: 変数 QueryResult
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:188: エラー: シンボルを見つけられません
[javac] } else if (queryResult == QueryResult.INVALID) {
[javac] ^
[javac] シンボル: 変数 QueryResult
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:189: エラー: シンボルを見つけられません
[javac] HashMap<Expr, Expr> model = getConcreteModel();
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:189: エラー: シンボルを見つけられません
[javac] HashMap<Expr, Expr> model = getConcreteModel();
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:234: エラー: シンボルを見つけられません
[javac] Expr stringVar = stringConstants.get(string);
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:264: エラー: シンボルを見つけられません
[javac] Expr value = model.get(variable);
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:280: エラー: シンボルを見つけられません
[javac] Op operator = value.getOp();
[javac] ^
[javac] シンボル: クラス Op
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:298: エラー: シンボルを見つけられません
[javac] List<Expr> varsAlreadySeen = Lists.newArrayList();
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:320: エラー: シンボルを見つけられません
[javac] List<Expr> varsAlreadySeen = Lists.newArrayList();
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:322: エラー: シンボルを見つけられません
[javac] Op charCons = lookupOp("char_cons");
[javac] ^
[javac] シンボル: クラス Op
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/Cvc3Context.java:323: エラー: シンボルを見つけられません
[javac] Expr charNil = lookupOp("char_nil").getExpr();
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス Cvc3Context
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/ApiBasedInputGenerator.java:52: エラー: シンボルを見つけられません
[javac] Set<Expr> assumptions = Sets.newHashSet();
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス ApiBasedInputGenerator
[javac] /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/src/symbolicexecutor/SymbolicValue.java:48: エラー: シンボルを見つけられません
[javac] Expr expr = context.lookupVar(name);
[javac] ^
[javac] シンボル: クラス Expr
[javac] 場所: クラス SymbolicValue
[javac] エラー72個
BUILD FAILED
/mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build.xml:69: Compile failed; see the compiler error output for details.
Total time: 27 secondsbuild.xml実行部分のターゲットcvc3
<target name="cvc3"
depends="configure-cvc3,check-config.status"
unless="config.status.present">
<exec dir="../cvc3" executable="/usr/bin/make"/>
<copy file="../cvc3/java/lib/${cvc3.jar}" todir="${lib.dir}" />
</target>
configure-cvc3、check-config.statusは完了している。
ので一度cvc3ターゲットを再現してみる
（antで実行できなかったものを、コマンドで実行する理由ってなんだろう？）
makeで凄い膨大な量のコメントが出る。
antで出ないのは、そういった仕様なんでしょうか。
いっぱい出ちゃうと、ant自体がどこまで進んだかわかりませんもんね。
makeの終わりの方のログ(続きより*2に全てのログ)
Unpacking parser
Unpacking translator
Unpacking vcl
Unpacking c_interface
cat UNPACKED | xargs g++ -shared -m64 -fPIC \
-Wl,-soname,libcvc3.so.3 -o '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0' `` -lgmp
/sbin/ldconfig -nv /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu
/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu:
<span style="color: #cc0000">libcvc3.so.3 -> libcvc3.so.3.0.0/sbin/ldconfig.real: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3 から libcvc3.so.3.0.0 へリンクできません</span>
(スキップされました)
ln -sf libcvc3.so.3.0.0 /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0
<span style="color: #cc0000">ln: シンボリックリンク `/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0' の作成に失敗しました: 読み込み専用ファイルシステムです</span>
<span style="color: #cc0000">make[2]: *** [/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0] エラー 1
</span>
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
make[1]: *** [build] エラー 2
make[1]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
make: *** [build] エラー 2
と、とりあえずmakefile読んでみる！(*makefile初心者)
（ところでこのようなエラーを見るのってどのくらい常識なんでしょうか・・。やはり問題が発生しない限り見ないもの？）
makefileには情報はなく、そこから色々なファイルを実行していてそれらを読む必要がありそう。
（先ほどのCVC3ターゲットのエラーの真の原因はここ？手当たり次第やるより、もう少し広く見た方がいいかも、まだcvc3ターゲットのどのコマンドが失敗だったか理解していない）
とりあえずlibのリンクがどこかに対してできていない。libcvc3.so.3.0.0ファイルは存在している
make[2]:***はよくわからないけどmakeじゃ検索できないし、エラーでも出てこないから標準出力かな？ググるも出てこない
直感だとlibcvc3.so.3リンクを張れていない事によるエラーをひきずっている気がする。
どこのシンボリックリンクを張れなかったのかはまだわからない。
(find再帰のお勉強)
maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ find -name libcvc3.so.3*
./lib/x86_64-linux-gnu/libcvc3.so.3.0.0
ファイルは見当たらず、エラーもまだわからない
grepで実行ファイルを洗い出しエラーの特定しかないかな（-）
今更だが、海外のソフトで日本語のエラーがでるはずがない事に気づく
日本語以外のログで検索せねば。
/usr/local/lib、javahome以下に無し
maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ grep -r libcvc3.so.3 バイナリファイル lib/x86_64-linux-gnu/libcvc3.so.3.0.0 に一致しました maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ ^C maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ grep -r libcvc3.so. INSTALL:variable) and both <code>libcvc3.so</code> and java/README:libcvc3.so (by default, /usr/local/lib) and the Java library into java/README:CLASSPATH environment variable) and both libcvc3.so and libcvc3jni.so java/README:Note that libcvc3.so and libcvc3jni.so may be installed into different java/README:3. libcvc3.so, as it is used by libcvc3jni.so java/README:Make sure that the version of libcvc3.so found at runtime has the same
cvc/java/READMEのヘルプ
http://js-symbolic-executor.googlecode.com/svn/trunk/cvc3/java/README
いずれにおいてもlibcvc3.soの説明ならあるが、libcvc3.so.3の説明は特になし
makeのログでlibcvc3を検索、ヒントになりそうな所はなし。
そういえば、make正確にはその他ファイルはどのようなログをはいているのだろうか。実行ログだったら参考になるが、そのようには所々コマンドのようでコマンドではないようなログもある
libcvc3.so.3は一般のファイルなのかなということでググってみる
ひっかかるのは大抵自分の質問（苦笑
ただ、似た種類だとrpmで落とせるのかな？
libcvc3.so.2なら落とせそうだけどなあ
rpm -ivh libcvc3.so.3 とはいかないしなあ
そもそもlivcvc3ってなんやねん！パッケージでやっている事をググっても出てこない。マイナーなファイルなのかな
rpmインストールして、パッケージ検索してみようかなんて遊んでたら
maru@marU:/$ sudo apt-get install libcvc3-
libcvc3-5 libcvc3-5-java libcvc3-5-jni libcvc3-dev
予測変換でちょっと関係ないのが出てきた
libcvc3って普通に落とせてインストールする関係のファイル？
少し戻って、makeの後は、コピーファイル。そのファイルが存在しないのでやっぱこのmakeの問題を解決しなければならないらしい（遅
うーん。rpmコマンド入れてみたけど、まだインストールしていないパッケージを探す方法はググってもない？直感だとありそうだけどなあ
次の手段は何だろう。そろそろ思いつかない
１．livcvc3.so.5と少し違うものをいれてみる
２．もともとjavaにもあるということで、他のJDKを入れてみる
３．make distcleanというおまじないをcvc以下で唱えてみる
とりあえず手頃なので前回失敗した理由のよくわからない、３番を試すだけ試す
なんかさっきよりも進んでるっぽい・・。もやもやする。
$ ../cvc3 make distclean
$ ../js-symbolic-executor ant (*1 続きより)
経緯
少し前に../js-symbolic-execution antを実行してcvc3ターゲットが実行できていない
cvc3ターゲットの初手の../cvc3 makeを実行する
../cvc3 make distcleanする
../js-symbolic-execution ant
ただのまやかしな気がします。
そもそも 初手のcvc3ターゲットをantで実行した際にmakeは実行されていたのでしょうか？いなかった気がする
ant終わったけど通っていませんでした。
出たエラーは同様のものでしたね。
２．のJDKについてwindows上のJdk 1.9.0,1.8_25,1.8.0_20にはありませんでしたね。
とりあえず今日は夜更かししすぎちゃったので、ここまで。
質問するにも質問が難しすぎる
libcvc3.so.3はどこから手に入りますか。と聞いても入手方法知ってる人いなさそう・・
続きはdistclean後のant(*1)とmake(*2)の全ログ
distclean後のant(*1)
maru@marU:/mnt/sharefolder/js-symbolic-executor/js-symbolic-executor$ ant
Buildfile: /mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build.xml
init:
closure-compiler:
compile:
[javac] /mnt/sharefolder/js-symbolic-executor/closure-compiler/build.xml:54: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
[javac] /mnt/sharefolder/js-symbolic-executor/closure-compiler/build.xml:60: warning: 'includeantruntime' was not set, defaulting to build.sysclasspath=last; set to false for repeatable builds
jar:
check-config.status:
configure-cvc3:
[exec] checking for g++... g++
[exec] checking whether the C++ compiler works... yes
[exec] checking for C++ compiler default output file name... a.out
[exec] checking for suffix of executables...
[exec] checking whether we are cross compiling... no
[exec] checking for suffix of object files... o
[exec] checking whether we are using the GNU C++ compiler... yes
[exec] checking whether g++ accepts -g... yes
[exec] checking how to run the C++ preprocessor... g++ -E
[exec] checking for ar... ar
[exec] checking build system type... x86_64-unknown-linux-gnu
[exec] checking host system type... x86_64-unknown-linux-gnu
[exec] checking for install... /usr/bin/install
[exec] checking for ldconfig... /sbin/ldconfig
[exec] checking for time... /usr/bin/time
[exec] checking for perl... /usr/bin/perl
[exec] checking for bison... bison -y
[exec] checking for flex... flex
[exec] checking lex output file root... lex.yy
[exec] checking lex library... none needed
[exec] checking whether yytext is a pointer... no
[exec] checking for compiler version (g++ --version)... 4.8.2
[exec] checking for gmp... yes
[exec] checking for javac... /usr/local/java/jdk1.8.0_40/bin/javac
[exec] checking for javah... /usr/local/java/jdk1.8.0_40/bin/javah
[exec] checking for jar... /usr/local/java/jdk1.8.0_40/bin/jar
[exec] checking for java... /usr/local/java/jdk1.8.0_40/bin/java
[exec] checking for grep that handles long lines and -e... /bin/grep
[exec] checking for egrep... /bin/grep -E
[exec] checking for ANSI C header files... yes
[exec] checking for sys/types.h... yes
[exec] checking for sys/stat.h... yes
[exec] checking for stdlib.h... yes
[exec] checking for string.h... yes
[exec] checking for memory.h... yes
[exec] checking for strings.h... yes
[exec] checking for inttypes.h... yes
[exec] checking for stdint.h... yes
[exec] checking for unistd.h... yes
[exec] checking jni.h usability... yes
[exec] checking jni.h presence... yes
[exec] checking for jni.h... yes
[exec] checking jni_md.h usability... yes
[exec] checking jni_md.h presence... yes
[exec] checking for jni_md.h... yes
[exec] checking for python... /usr/bin/python
[exec] checking vector usability... yes
[exec] checking vector presence... yes
[exec] checking for vector... yes
[exec] checking list usability... yes
[exec] checking list presence... yes
[exec] checking for list... yes
[exec] checking deque usability... yes
[exec] checking deque presence... yes
[exec] checking for deque... yes
[exec] checking set usability... yes
[exec] checking set presence... yes
[exec] checking for set... yes
[exec] checking string usability... yes
[exec] checking string presence... yes
[exec] checking for string... yes
[exec] checking cstdlib usability... yes
[exec] checking cstdlib presence... yes
[exec] checking for cstdlib... yes
[exec] checking cstdio usability... yes
[exec] checking cstdio presence... yes
[exec] checking for cstdio... yes
[exec] checking functional usability... yes
[exec] checking functional presence... yes
[exec] checking for functional... yes
[exec] checking algorithm usability... yes
[exec] checking algorithm presence... yes
[exec] checking for algorithm... yes
[exec] checking for doxygen... no
[exec] checking for doxytag... no
[exec] checking for fig2dev... no
[exec] checking for dot... NO
[exec] checking for etags... no
[exec] checking for ebrowse... no
[exec] configure: creating ./config.status
[exec] config.status: creating Makefile.local
[exec] config.status: creating LICENSE
[exec] config.status: creating src/cvc3.pc
[exec] config.status: creating bin/unpack
[exec] config.status: creating bin/run_tests
[exec] config.status: creating bin/cvc2smt
[exec] config.status: creating doc/Doxyfile
[exec] config.status: creating doc/Makefile
[exec]
[exec] CVC3 is configured successfully.
[exec] Platform: x86_64-linux-gnu
[exec] Version: 2010-09-02
[exec] Computer arithmetic: GMP
[exec]
[exec] Run ./configure --help for additional configuration options.
[exec]
[exec] Type 'make' to compile CVC3.
[exec]
[exec] *** CVC3 is configured to compile using shared libraries.
[exec] *** Type "make ld_sh" for bash shells or "make ld_csh" for csh shells
[exec] *** to see how to set LD_LIBRARY_PATH appropriately. To use static
[exec] *** libraries and executables instead, run:
[exec] *** ./configure --enable-static
cvc3:
[exec] cd /mnt/sharefolder/js-symbolic-executor/cvc3/src; /usr/bin/make VERSION=2010-09-02
[exec] make[1]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' に入ります
[exec] cd util && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/util' に入ります
[exec] Making dependencies for debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/util' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/util' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c debug.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/debug.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c statistics.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/statistics.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c rational.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c rational-native.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-native.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c rational-gmp.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-gmp.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc_util.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc_util.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/debug.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/statistics.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-native.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-gmp.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/debug.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/statistics.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-native.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-gmp.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/util' から出ます
[exec] cd context && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/context' に入ります
[exec] Making dependencies for context.cpp cdflags.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include context.cpp cdflags.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/context' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/context' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c context.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/context.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c cdflags.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/cdflags.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcontext.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcontext.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/context.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/cdflags.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/context.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/cdflags.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/context' から出ます
[exec] cd expr && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/expr' に入ります
[exec] Making dependencies for expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/expr' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/expr' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_manager.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_manager.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_stream.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_stream.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_value.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_value.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_op.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_op.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libexpr.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libexpr.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_manager.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_stream.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_value.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_op.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_manager.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_stream.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_value.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_op.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/expr' から出ます
[exec] cd theorem && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theorem' に入ります
[exec] Making dependencies for assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theorem' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theorem' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c assumptions.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/assumptions.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theorem.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theorem_manager.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_manager.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_producer.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c common_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o'
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheorem.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/assumptions.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_manager.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheorem.a を作成しています
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/assumptions.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_manager.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theorem' から出ます
[exec] cd sat && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/sat' に入ります
[exec] Making dependencies for cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/sat' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/sat' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c cnf.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c cnf_manager.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_manager.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c cnf_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c dpllt_basic.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_basic.o'
[exec] dpllt_basic.cpp: In member function ‘void SAT::DPLLTBasic::handle_result(SatSolver::SATStatus)’:
[exec] dpllt_basic.cpp:172:16: warning: variable ‘result’ set but not used [-Wunused-but-set-variable]
[exec] const char * result = "UNKNOWN";
[exec] ^
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c sat_api.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/sat_api.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c dpllt_minisat.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_minisat.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c minisat_types.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_types.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c minisat_derivation.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_derivation.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c minisat_solver.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_solver.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsat.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsat.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_manager.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_basic.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/sat_api.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_minisat.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_types.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_derivation.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_solver.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_manager.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_basic.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/sat_api.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_minisat.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_types.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_derivation.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_solver.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/sat' から出ます
[exec] cd theory_core && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_core' に入ります
[exec] Making dependencies for theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_core' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_core' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_core.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory_core.o'
[exec] theory_core.cpp: In constructor ‘CVC3::TheoryCore::TheoryCore(CVC3::ContextManager*, CVC3::ExprManager*, CVC3::TheoremManager*, CVC3::Translator*, const CVC3::CLFlags&, CVC3::Statistics&)’:
[exec] theory_core.cpp:722:22: warning: converting ‘false’ to pointer type ‘const bool*’ [-Wconversion-null]
[exec] d_coreSatAPI(NULL)
[exec] ^
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c core_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_transform.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/expr_transform.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c bryant.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/bryant.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_core.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_core.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory_core.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/expr_transform.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/bryant.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory_core.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/expr_transform.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/bryant.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_core' から出ます
[exec] cd theory_arith && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_arith' に入ります
[exec] Making dependencies for arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_arith' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_arith' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c arith_theorem_producer_old.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c arith_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c arith_theorem_producer3.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_arith.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_arith_old.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o'
[exec] theory_arith_old.cpp: In member function ‘virtual void CVC3::TheoryArithOld::checkSat(bool)’:
[exec] theory_arith_old.cpp:2699:10: warning: variable ‘something_enqueued’ set but not used [-Wunused-but-set-variable]
[exec] bool something_enqueued = false;
[exec] ^
[exec] theory_arith_old.cpp: In member function ‘bool CVC3::TheoryArithOld::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’:
[exec] theory_arith_old.cpp:2851:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable]
[exec] bool strictLB=false, strictUB=false;
[exec] ^
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_arith_new.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o'
[exec] theory_arith_new.cpp: In member function ‘bool CVC3::TheoryArithNew::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’:
[exec] theory_arith_new.cpp:1350:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable]
[exec] bool strictLB=false, strictUB=false;
[exec] ^
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_arith3.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o'
[exec] theory_arith3.cpp: In member function ‘bool CVC3::TheoryArith3::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’:
[exec] theory_arith3.cpp:2199:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable]
[exec] bool strictLB=false, strictUB=false;
[exec] ^
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_arith.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_arith.a を作成しています
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_arith' から出ます
[exec] cd theory_array && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_array' に入ります
[exec] Making dependencies for array_theorem_producer.cpp theory_array.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include array_theorem_producer.cpp theory_array.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_array' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_array' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c array_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_array.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/theory_array.o'
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_array.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/theory_array.o
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_array.a を作成しています
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/theory_array.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_array' から出ます
[exec] cd theory_bitvector && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_bitvector' に入ります
[exec] Making dependencies for bitvector_theorem_producer.cpp theory_bitvector.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include bitvector_theorem_producer.cpp theory_bitvector.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_bitvector' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_bitvector' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c bitvector_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_bitvector.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o'
[exec] theory_bitvector.cpp: In member function ‘CVC3::Theorem CVC3::TheoryBitvector::rewriteBV(const CVC3::Expr&, CVC3::ExprMap<CVC3::Theorem>&, int)’:
[exec] theory_bitvector.cpp:1063:11: warning: variable ‘hi’ set but not used [-Wunused-but-set-variable]
[exec] int hi(-1), low(-1);
[exec] ^
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_bitvector.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_bitvector.a を作成しています
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_bitvector' から出ます
[exec] cd theory_datatype && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_datatype' に入ります
[exec] Making dependencies for datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_datatype' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_datatype' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c datatype_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_datatype.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_datatype_lazy.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_datatype.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_datatype.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_datatype' から出ます
[exec] cd theory_quant && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_quant' に入ります
[exec] Making dependencies for theory_quant.cpp quant_theorem_producer.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include theory_quant.cpp quant_theorem_producer.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_quant' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_quant' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_quant.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/theory_quant.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c quant_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_quant.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_quant.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/theory_quant.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/theory_quant.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_quant' から出ます
[exec] cd theory_records && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_records' に入ります
[exec] Making dependencies for theory_records.cpp records_theorem_producer.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include theory_records.cpp records_theorem_producer.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_records' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_records' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_records.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/theory_records.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c records_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_records.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_records.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/theory_records.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/theory_records.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_records' から出ます
[exec] cd theory_simulate && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_simulate' に入ります
[exec] Making dependencies for theory_simulate.cpp simulate_theorem_producer.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include theory_simulate.cpp simulate_theorem_producer.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_simulate' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_simulate' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_simulate.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c simulate_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o'
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_simulate.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_simulate.a を作成しています
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_simulate' から出ます
[exec] cd theory_uf && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_uf' に入ります
[exec] Making dependencies for uf_theorem_producer.cpp theory_uf.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include uf_theorem_producer.cpp theory_uf.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_uf' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_uf' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c uf_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_uf.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/theory_uf.o'
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_uf.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/theory_uf.o
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_uf.a を作成しています
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/theory_uf.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_uf' から出ます
[exec] cd search && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/search' に入ります
[exec] Making dependencies for clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/search' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/search' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c clause.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/clause.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_impl_base.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_impl_base.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_fast.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_fast.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_theorem_producer.o'
[exec] search_theorem_producer.cpp: In member function ‘CVC3::Expr CVC3::SearchEngineTheoremProducer::convertToCNF(const CVC3::Expr&, const CVC3::Expr&)’:
[exec] search_theorem_producer.cpp:1317:17: warning: unused variable ‘negV’ [-Wunused-variable]
[exec] const Expr& negV = v.negate();
[exec] ^
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_sat.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_sat.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_simple.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_simple.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c variable.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/variable.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c circuit.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/circuit.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c decision_engine.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c decision_engine_dfs.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine_dfs.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCObject.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCObject.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCUtilProof.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCUtilProof.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCBoolProof.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCBoolProof.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCConvert.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCConvert.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCLraProof.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCLraProof.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCPrinter.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCPrinter.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCProof.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCProof.o'
[exec] LFSCProof.cpp: In member function ‘virtual int LFSCProof::checkOp()’:
[exec] LFSCProof.cpp:91:11: warning: unused variable ‘o’ [-Wunused-variable]
[exec] int o = getChild( a )->checkOp();
[exec] ^
[exec] LFSCProof.cpp: In static member function ‘static LFSCProof* LFSCProof::Make_CNF(const CVC3::Expr&, const CVC3::Expr&, int)’:
[exec] LFSCProof.cpp:193:11: warning: unused variable ‘m2’ [-Wunused-variable]
[exec] int m2 = queryM( ec[1] );
[exec] ^
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c TReturn.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/TReturn.o'
[exec] TReturn.cpp: In static member function ‘static int TReturn::normalize_tr(const CVC3::Expr&, TReturn*&, int, bool, bool)’:
[exec] TReturn.cpp:127:12: warning: unused variable ‘torig’ [-Wunused-variable]
[exec] TReturn* torig = t1;
[exec] ^
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c Util.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/Util.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsearch.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsearch.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/clause.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_impl_base.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_fast.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_sat.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_simple.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/variable.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/circuit.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine_dfs.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCObject.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCUtilProof.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCBoolProof.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCConvert.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCLraProof.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCPrinter.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCProof.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/TReturn.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/Util.o
[exec] PL.y: 警告: 3 shift/reduce conflicts [-Wconflicts-sr]
[exec] PL.y:1531.24-1536.25: 警告: 衝突のせいでパーサ内の規則が使用できません [-Wother]
[exec] AndExpr : AndExpr AND_TOK Expr
[exec] ^^^^^^^^^^^^^
[exec] PL.y:1549.25-1554.25: 警告: 衝突のせいでパーサ内の規則が使用できません [-Wother]
[exec] OrExpr : OrExpr OR_TOK Expr
[exec] ^^^^^^^^^^
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/clause.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_impl_base.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_fast.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_theorem_producer.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_sat.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_simple.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/variable.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/circuit.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine_dfs.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCObject.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCUtilProof.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCBoolProof.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCConvert.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCLraProof.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCPrinter.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCProof.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/TReturn.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/Util.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/search' から出ます
[exec] cd parser && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/parser' に入ります
[exec] bison -d -y -o parsePL.cpp -p PL --debug -v PL.y
[exec] flex -I -PPL -olexPL.cpp PL.lex
[exec] bison -d -y -o parseLisp.cpp -p Lisp --debug -v Lisp.y
[exec] flex -I -PLisp -olexLisp.cpp Lisp.lex
[exec] bison -d -y -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y
[exec] flex -I -Psmtlib -olexsmtlib.cpp smtlib.lex
[exec] smtlib2.y: 警告: 4 shift/reduce conflicts [-Wconflicts-sr]
[exec] bison -d -y -o parsesmtlib2.cpp -p smtlib2 --debug -v smtlib2.y
[exec] flex -I -Psmtlib2 -olexsmtlib2.cpp smtlib2.lex
[exec] Making dependencies for parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/parser' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/parser' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parsePL.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsePL.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c lexPL.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexPL.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parseLisp.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parseLisp.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c lexLisp.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexLisp.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parsesmtlib.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c lexsmtlib.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parsesmtlib2.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib2.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c lexsmtlib2.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib2.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parser.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parser.o'
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libparser.a を作成しています
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libparser.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsePL.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexPL.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parseLisp.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexLisp.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib2.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib2.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parser.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsePL.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexPL.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parseLisp.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexLisp.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib2.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib2.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parser.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/parser' から出ます
[exec] cd translator && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/translator' に入ります
[exec] Making dependencies for translator.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include translator.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/translator/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/translator' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/translator' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c translator.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/translator/x86_64-linux-gnu/translator.o'
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtranslator.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/translator/x86_64-linux-gnu/translator.o
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtranslator.a を作成しています
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/translator/x86_64-linux-gnu/translator.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/translator' から出ます
[exec] cd vcl && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/vcl' に入ります
[exec] Making dependencies for vcl.cpp vc_cmd.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include vcl.cpp vc_cmd.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/vcl' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/vcl' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c vcl.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vcl.o'
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c vc_cmd.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vc_cmd.o'
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libvcl.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vcl.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vc_cmd.o
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libvcl.a を作成しています
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vcl.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vc_cmd.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/vcl' から出ます
[exec] cd c_interface && /usr/bin/make
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/c_interface' に入ります
[exec] Making dependencies for c_interface.cpp
[exec] g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include c_interface.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/c_interface/x86_64-linux-gnu/Makefile.tmp
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/c_interface' から出ます
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/c_interface' に入ります
[exec] g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c c_interface.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/c_interface/x86_64-linux-gnu/c_interface.o'
[exec] c_interface.cpp: In function ‘void* vc_bvWriteToMemoryArray(VC, Expr, Expr, Expr, int)’:
[exec] c_interface.cpp:2020:9: warning: variable ‘hi’ set but not used [-Wunused-but-set-variable]
[exec] int hi = newBitsPerElem - 1;
[exec] ^
[exec] ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libc_interface.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/c_interface/x86_64-linux-gnu/c_interface.o
[exec] a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/c_interface/x86_64-linux-gnu/c_interface.o
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/c_interface' から出ます
[exec] /usr/bin/make /mnt/sharefolder/js-symbolic-executor/cvc3/lib/libcvc3.so.3.0.0
[exec] ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libc_interface.a を作成しています
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' に入ります
[exec] Building shared library /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0
[exec] rm -rf /mnt/sharefolder/js-symbolic-executor/cvc3/unpack_tmp
[exec] /mnt/sharefolder/js-symbolic-executor/cvc3/bin/unpack /mnt/sharefolder/js-symbolic-executor/cvc3/unpack_tmp /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc_util.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcontext.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libexpr.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheorem.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsat.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_core.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_arith.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_array.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_bitvector.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_datatype.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_quant.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_records.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_simulate.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_uf.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsearch.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libparser.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtranslator.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libvcl.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libc_interface.a > UNPACKED
[exec] Found 86 members in 19 libraries
[exec] Unpacking cvc_util
[exec] Unpacking context
[exec] Unpacking expr
[exec] Unpacking theorem
[exec] Unpacking sat
[exec] Unpacking theory_core
[exec] Unpacking theory_arith
[exec] Unpacking theory_array
[exec] Unpacking theory_bitvector
[exec] Unpacking theory_datatype
[exec] Unpacking theory_quant
[exec] Unpacking theory_records
[exec] Unpacking theory_simulate
[exec] Unpacking theory_uf
[exec] Unpacking search
[exec] Unpacking parser
[exec] Unpacking translator
[exec] Unpacking vcl
[exec] Unpacking c_interface
[exec] cat UNPACKED | xargs g++ -shared -m64 -fPIC \
[exec] -Wl,-soname,libcvc3.so.3 -o '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0' `` -lgmp
[exec] /sbin/ldconfig -nv /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu
[exec] /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu:
[exec] libcvc3.so.3 -> libcvc3.so.3.0.0 (スキップされました)
[exec] ln -sf libcvc3.so.3.0.0 /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0
[exec] make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
[exec] make[1]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
[exec] /sbin/ldconfig.real: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3 から libcvc3.so.3.0.0 へリンクできません
[exec] ln: シンボリックリンク `/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0' の作成に失敗しました: 読み込み専用ファイルシステムです
[exec] make[2]: *** [/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0] エラー 1
[exec] make[1]: *** [build] エラー 2
[exec] make: *** [build] エラー 2
[exec] Result: 2
BUILD FAILED
/mnt/sharefolder/js-symbolic-executor/js-symbolic-executor/build.xml:116: Warning: Could not find file /mnt/sharefolder/js-symbolic-executor/cvc3/java/lib/libcvc3-3.0.0.jar to copy.
Total time: 8 minutes 9 secondsちょっと前のmakeログ(*2)
念のためmakeの全ログ（自分用）
maru@marU:/mnt/sharefolder/js-symbolic-executor/cvc3$ /usr/bin/make
cd /mnt/sharefolder/js-symbolic-executor/cvc3/src; /usr/bin/make VERSION=2010-09-02
make[1]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' に入ります
cd util && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/util' に入ります
Making dependencies for debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP debug.cpp statistics.cpp rational.cpp rational-native.cpp rational-gmp.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/util' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/util' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c debug.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/debug.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c statistics.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/statistics.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c rational.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c rational-native.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-native.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -DRATIONAL_GMP -c rational-gmp.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-gmp.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc_util.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/debug.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/statistics.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-native.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-gmp.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc_util.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/debug.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/statistics.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-native.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/util/x86_64-linux-gnu/rational-gmp.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/util' から出ます
cd context && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/context' に入ります
Making dependencies for context.cpp cdflags.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include context.cpp cdflags.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/context' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/context' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c context.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/context.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c cdflags.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/cdflags.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcontext.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/context.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/cdflags.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcontext.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/context.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/context/x86_64-linux-gnu/cdflags.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/context' から出ます
cd expr && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/expr' に入ります
Making dependencies for expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include expr.cpp expr_manager.cpp expr_stream.cpp expr_value.cpp expr_op.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/expr' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/expr' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_manager.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_manager.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_stream.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_stream.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_value.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_value.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_op.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_op.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libexpr.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_manager.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_stream.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_value.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_op.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libexpr.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_manager.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_stream.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_value.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/expr/x86_64-linux-gnu/expr_op.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/expr' から出ます
cd theorem && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theorem' に入ります
Making dependencies for assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include assumptions.cpp theorem.cpp theorem_manager.cpp theorem_producer.cpp common_theorem_producer.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theorem' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theorem' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c assumptions.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/assumptions.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theorem.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theorem_manager.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_manager.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c common_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheorem.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/assumptions.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_manager.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheorem.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/assumptions.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_manager.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theorem/x86_64-linux-gnu/common_theorem_producer.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theorem' から出ます
cd sat && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/sat' に入ります
Making dependencies for cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include cnf.cpp cnf_manager.cpp cnf_theorem_producer.cpp dpllt_basic.cpp sat_api.cpp dpllt_minisat.cpp minisat_types.cpp minisat_derivation.cpp minisat_solver.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/sat' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/sat' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c cnf.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c cnf_manager.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_manager.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c cnf_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c dpllt_basic.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_basic.o'
dpllt_basic.cpp: In member function ‘void SAT::DPLLTBasic::handle_result(SatSolver::SATStatus)’:
dpllt_basic.cpp:172:16: warning: variable ‘result’ set but not used [-Wunused-but-set-variable]
const char * result = "UNKNOWN";
^
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c sat_api.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/sat_api.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c dpllt_minisat.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_minisat.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c minisat_types.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_types.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c minisat_derivation.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_derivation.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c minisat_solver.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_solver.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsat.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_manager.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_basic.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/sat_api.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_minisat.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_types.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_derivation.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_solver.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsat.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_manager.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/cnf_theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_basic.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/sat_api.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/dpllt_minisat.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_types.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_derivation.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/sat/x86_64-linux-gnu/minisat_solver.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/sat' から出ます
cd theory_core && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_core' に入ります
Making dependencies for theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include theory.cpp theory_core.cpp core_theorem_producer.cpp expr_transform.cpp bryant.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_core' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_core' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_core.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory_core.o'
theory_core.cpp: In constructor ‘CVC3::TheoryCore::TheoryCore(CVC3::ContextManager*, CVC3::ExprManager*, CVC3::TheoremManager*, CVC3::Translator*, const CVC3::CLFlags&, CVC3::Statistics&)’:
theory_core.cpp:722:22: warning: converting ‘false’ to pointer type ‘const bool*’ [-Wconversion-null]
d_coreSatAPI(NULL)
^
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c core_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c expr_transform.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/expr_transform.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c bryant.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/bryant.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_core.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory_core.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/expr_transform.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/bryant.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_core.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/theory_core.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/core_theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/expr_transform.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_core/x86_64-linux-gnu/bryant.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_core' から出ます
cd theory_arith && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_arith' に入ります
Making dependencies for arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include arith_theorem_producer_old.cpp arith_theorem_producer.cpp arith_theorem_producer3.cpp theory_arith.cpp theory_arith_old.cpp theory_arith_new.cpp theory_arith3.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_arith' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_arith' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c arith_theorem_producer_old.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c arith_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c arith_theorem_producer3.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_arith.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_arith_old.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o'
theory_arith_old.cpp: In member function ‘virtual void CVC3::TheoryArithOld::checkSat(bool)’:
theory_arith_old.cpp:2699:10: warning: variable ‘something_enqueued’ set but not used [-Wunused-but-set-variable]
bool something_enqueued = false;
^
theory_arith_old.cpp: In member function ‘bool CVC3::TheoryArithOld::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’:
theory_arith_old.cpp:2851:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable]
bool strictLB=false, strictUB=false;
^
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_arith_new.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o'
theory_arith_new.cpp: In member function ‘bool CVC3::TheoryArithNew::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’:
theory_arith_new.cpp:1350:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable]
bool strictLB=false, strictUB=false;
^
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_arith3.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o'
theory_arith3.cpp: In member function ‘bool CVC3::TheoryArith3::findBounds(const CVC3::Expr&, CVC3::Rational&, CVC3::Rational&)’:
theory_arith3.cpp:2199:24: warning: variable ‘strictUB’ set but not used [-Wunused-but-set-variable]
bool strictLB=false, strictUB=false;
^
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_arith.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_arith.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer_old.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/arith_theorem_producer3.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_old.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith_new.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_arith/x86_64-linux-gnu/theory_arith3.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_arith' から出ます
cd theory_array && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_array' に入ります
Making dependencies for array_theorem_producer.cpp theory_array.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include array_theorem_producer.cpp theory_array.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_array' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_array' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c array_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_array.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/theory_array.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_array.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/theory_array.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_array.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/array_theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_array/x86_64-linux-gnu/theory_array.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_array' から出ます
cd theory_bitvector && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_bitvector' に入ります
Making dependencies for bitvector_theorem_producer.cpp theory_bitvector.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include bitvector_theorem_producer.cpp theory_bitvector.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_bitvector' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_bitvector' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c bitvector_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_bitvector.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o'
theory_bitvector.cpp: In member function ‘CVC3::Theorem CVC3::TheoryBitvector::rewriteBV(const CVC3::Expr&, CVC3::ExprMap<CVC3::Theorem>&, int)’:
theory_bitvector.cpp:1063:11: warning: variable ‘hi’ set but not used [-Wunused-but-set-variable]
int hi(-1), low(-1);
^
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_bitvector.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_bitvector.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/bitvector_theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_bitvector/x86_64-linux-gnu/theory_bitvector.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_bitvector' から出ます
cd theory_datatype && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_datatype' に入ります
Making dependencies for datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include datatype_theorem_producer.cpp theory_datatype.cpp theory_datatype_lazy.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_datatype' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_datatype' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c datatype_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_datatype.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_datatype_lazy.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_datatype.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_datatype.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/datatype_theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_datatype/x86_64-linux-gnu/theory_datatype_lazy.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_datatype' から出ます
cd theory_quant && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_quant' に入ります
Making dependencies for theory_quant.cpp quant_theorem_producer.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include theory_quant.cpp quant_theorem_producer.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_quant' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_quant' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_quant.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/theory_quant.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c quant_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_quant.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/theory_quant.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_quant.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/theory_quant.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_quant/x86_64-linux-gnu/quant_theorem_producer.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_quant' から出ます
cd theory_records && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_records' に入ります
Making dependencies for theory_records.cpp records_theorem_producer.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include theory_records.cpp records_theorem_producer.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_records' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_records' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_records.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/theory_records.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c records_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_records.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/theory_records.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_records.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/theory_records.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_records/x86_64-linux-gnu/records_theorem_producer.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_records' から出ます
cd theory_simulate && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_simulate' に入ります
Making dependencies for theory_simulate.cpp simulate_theorem_producer.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include theory_simulate.cpp simulate_theorem_producer.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_simulate' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_simulate' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_simulate.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c simulate_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_simulate.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_simulate.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/theory_simulate.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_simulate/x86_64-linux-gnu/simulate_theorem_producer.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_simulate' から出ます
cd theory_uf && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_uf' に入ります
Making dependencies for uf_theorem_producer.cpp theory_uf.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include uf_theorem_producer.cpp theory_uf.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_uf' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_uf' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c uf_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c theory_uf.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/theory_uf.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_uf.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/theory_uf.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_uf.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/uf_theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/theory_uf/x86_64-linux-gnu/theory_uf.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/theory_uf' から出ます
cd search && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/search' に入ります
Making dependencies for clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include clause.cpp search_impl_base.cpp search.cpp search_fast.cpp search_theorem_producer.cpp search_sat.cpp search_simple.cpp variable.cpp circuit.cpp decision_engine.cpp decision_engine_dfs.cpp LFSCObject.cpp LFSCUtilProof.cpp LFSCBoolProof.cpp LFSCConvert.cpp LFSCLraProof.cpp LFSCPrinter.cpp LFSCProof.cpp TReturn.cpp Util.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/search' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/search' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c clause.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/clause.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_impl_base.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_impl_base.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_fast.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_fast.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_theorem_producer.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_theorem_producer.o'
search_theorem_producer.cpp: In member function ‘CVC3::Expr CVC3::SearchEngineTheoremProducer::convertToCNF(const CVC3::Expr&, const CVC3::Expr&)’:
search_theorem_producer.cpp:1317:17: warning: unused variable ‘negV’ [-Wunused-variable]
const Expr& negV = v.negate();
^
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_sat.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_sat.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c search_simple.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_simple.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c variable.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/variable.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c circuit.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/circuit.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c decision_engine.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c decision_engine_dfs.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine_dfs.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCObject.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCObject.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCUtilProof.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCUtilProof.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCBoolProof.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCBoolProof.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCConvert.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCConvert.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCLraProof.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCLraProof.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCPrinter.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCPrinter.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c LFSCProof.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCProof.o'
LFSCProof.cpp: In member function ‘virtual int LFSCProof::checkOp()’:
LFSCProof.cpp:91:11: warning: unused variable ‘o’ [-Wunused-variable]
int o = getChild( a )->checkOp();
^
LFSCProof.cpp: In static member function ‘static LFSCProof* LFSCProof::Make_CNF(const CVC3::Expr&, const CVC3::Expr&, int)’:
LFSCProof.cpp:193:11: warning: unused variable ‘m2’ [-Wunused-variable]
int m2 = queryM( ec[1] );
^
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c TReturn.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/TReturn.o'
TReturn.cpp: In static member function ‘static int TReturn::normalize_tr(const CVC3::Expr&, TReturn*&, int, bool, bool)’:
TReturn.cpp:127:12: warning: unused variable ‘torig’ [-Wunused-variable]
TReturn* torig = t1;
^
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c Util.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/Util.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsearch.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/clause.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_impl_base.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_fast.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_theorem_producer.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_sat.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_simple.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/variable.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/circuit.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine_dfs.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCObject.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCUtilProof.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCBoolProof.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCConvert.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCLraProof.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCPrinter.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCProof.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/TReturn.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/Util.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsearch.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/clause.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_impl_base.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_fast.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_theorem_producer.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_sat.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/search_simple.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/variable.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/circuit.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/decision_engine_dfs.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCObject.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCUtilProof.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCBoolProof.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCConvert.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCLraProof.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCPrinter.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/LFSCProof.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/TReturn.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/search/x86_64-linux-gnu/Util.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/search' から出ます
cd parser && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/parser' に入ります
bison -d -y -o parsePL.cpp -p PL --debug -v PL.y
PL.y: 警告: 3 shift/reduce conflicts [-Wconflicts-sr]
PL.y:1531.24-1536.25: 警告: 衝突のせいでパーサ内の規則が使用できません [-Wother]
AndExpr : AndExpr AND_TOK Expr
^^^^^^^^^^^^^
PL.y:1549.25-1554.25: 警告: 衝突のせいでパーサ内の規則が使用できません [-Wother]
OrExpr : OrExpr OR_TOK Expr
^^^^^^^^^^
flex -I -PPL -olexPL.cpp PL.lex
bison -d -y -o parseLisp.cpp -p Lisp --debug -v Lisp.y
flex -I -PLisp -olexLisp.cpp Lisp.lex
bison -d -y -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y
flex -I -Psmtlib -olexsmtlib.cpp smtlib.lex
bison -d -y -o parsesmtlib2.cpp -p smtlib2 --debug -v smtlib2.y
smtlib2.y: 警告: 4 shift/reduce conflicts [-Wconflicts-sr]
flex -I -Psmtlib2 -olexsmtlib2.cpp smtlib2.lex
Making dependencies for parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 parsePL.cpp lexPL.cpp parseLisp.cpp lexLisp.cpp parsesmtlib.cpp lexsmtlib.cpp parsesmtlib2.cpp lexsmtlib2.cpp parser.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/parser' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/parser' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parsePL.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsePL.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c lexPL.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexPL.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parseLisp.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parseLisp.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c lexLisp.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexLisp.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parsesmtlib.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c lexsmtlib.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parsesmtlib2.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib2.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c lexsmtlib2.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib2.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -O0 -c parser.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parser.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libparser.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsePL.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexPL.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parseLisp.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexLisp.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib2.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib2.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parser.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libparser.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsePL.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexPL.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parseLisp.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexLisp.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parsesmtlib2.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/lexsmtlib2.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/parser/x86_64-linux-gnu/parser.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/parser' から出ます
cd translator && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/translator' に入ります
Making dependencies for translator.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include translator.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/translator/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/translator' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/translator' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c translator.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/translator/x86_64-linux-gnu/translator.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtranslator.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/translator/x86_64-linux-gnu/translator.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtranslator.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/translator/x86_64-linux-gnu/translator.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/translator' から出ます
cd vcl && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/vcl' に入ります
Making dependencies for vcl.cpp vc_cmd.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include vcl.cpp vc_cmd.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/vcl' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/vcl' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c vcl.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vcl.o'
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c vc_cmd.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vc_cmd.o'
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libvcl.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vcl.o /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vc_cmd.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libvcl.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vcl.o
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/vcl/x86_64-linux-gnu/vc_cmd.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/vcl' から出ます
cd c_interface && /usr/bin/make
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/c_interface' に入ります
Making dependencies for c_interface.cpp
g++ -M -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include c_interface.cpp >> /mnt/sharefolder/js-symbolic-executor/cvc3/obj/c_interface/x86_64-linux-gnu/Makefile.tmp
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/c_interface' から出ます
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/c_interface' に入ります
g++ -m64 -fPIC -O2 -Wall -I. -I/mnt/sharefolder/js-symbolic-executor/cvc3/src/include -c c_interface.cpp -o '/mnt/sharefolder/js-symbolic-executor/cvc3/obj/c_interface/x86_64-linux-gnu/c_interface.o'
c_interface.cpp: In function ‘void* vc_bvWriteToMemoryArray(VC, Expr, Expr, Expr, int)’:
c_interface.cpp:2020:9: warning: variable ‘hi’ set but not used [-Wunused-but-set-variable]
int hi = newBitsPerElem - 1;
^
ar ruvs '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libc_interface.a' /mnt/sharefolder/js-symbolic-executor/cvc3/obj/c_interface/x86_64-linux-gnu/c_interface.o
ar: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libc_interface.a を作成しています
a - /mnt/sharefolder/js-symbolic-executor/cvc3/obj/c_interface/x86_64-linux-gnu/c_interface.o
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src/c_interface' から出ます
/usr/bin/make /mnt/sharefolder/js-symbolic-executor/cvc3/lib/libcvc3.so.3.0.0
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' に入ります
Building shared library /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0
rm -rf /mnt/sharefolder/js-symbolic-executor/cvc3/unpack_tmp
/mnt/sharefolder/js-symbolic-executor/cvc3/bin/unpack /mnt/sharefolder/js-symbolic-executor/cvc3/unpack_tmp /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc_util.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcontext.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libexpr.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheorem.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsat.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_core.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_arith.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_array.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_bitvector.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_datatype.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_quant.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_records.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_simulate.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtheory_uf.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libsearch.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libparser.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libtranslator.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libvcl.a /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libc_interface.a > UNPACKED
Found 86 members in 19 libraries
Unpacking cvc_util
Unpacking context
Unpacking expr
Unpacking theorem
Unpacking sat
Unpacking theory_core
Unpacking theory_arith
Unpacking theory_array
Unpacking theory_bitvector
Unpacking theory_datatype
Unpacking theory_quant
Unpacking theory_records
Unpacking theory_simulate
Unpacking theory_uf
Unpacking search
Unpacking parser
Unpacking translator
Unpacking vcl
Unpacking c_interface
cat UNPACKED | xargs g++ -shared -m64 -fPIC \
-Wl,-soname,libcvc3.so.3 -o '/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0' `` -lgmp
/sbin/ldconfig -nv /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu
/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu:
libcvc3.so.3 -> libcvc3.so.3.0.0/sbin/ldconfig.real: /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3 から libcvc3.so.3.0.0 へリンクできません
(スキップされました)
ln -sf libcvc3.so.3.0.0 /mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0
ln: シンボリックリンク `/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0' の作成に失敗しました: 読み込み専用ファイルシステムです
make[2]: *** [/mnt/sharefolder/js-symbolic-executor/cvc3/lib/x86_64-linux-gnu/libcvc3.so.3.0.0] エラー 1
make[2]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
make[1]: *** [build] エラー 2
make[1]: ディレクトリ `/mnt/sharefolder/js-symbolic-executor/cvc3/src' から出ます
make: *** [build] エラー 2
