Fix carbon backend

deps/boogie/2012-10-22/unix/bin/boogie

@@ -32,6 +32,15 @@ function doargs(){
 BOOGIE_HOME=`dirname "$0"`
 BOOGIE_HOME=`dirname "$BOOGIE_HOME"`
 
+if [ "X$BOOGIE_Z3_EXE" == "X" ] ; then
+    BOOGIE_Z3_EXE=`dirname "$BOOGIE_HOME"`
+    BOOGIE_Z3_EXE=`dirname "$BOOGIE_Z3_EXE"`
+    BOOGIE_Z3_EXE=`dirname "$BOOGIE_Z3_EXE"`
+    export BOOGIE_Z3_EXE=$BOOGIE_Z3_EXE/z3/4.3.1/`uname -s`/x86_64/bin/z3
+fi
+
+#echo $BOOGIE_Z3_EXE
+
 # we append stderr to stdout, because chalice acts weird
 # if there is any output on stderr.
 exec mono $BOOGIE_HOME/Boogie.exe `doargs "$@"` 2>&1

viper/carbon/src/main/scala/viper/api/CarbonVerifier.scala

@@ -11,14 +11,18 @@ class CarbonVerifier[O,Err](o:OriginFactory[O]) extends SilverImplementation[O,E
     } else if(OS.startsWith("Mac")){
       tool_home.resolve("z3").resolve("4.3.1").resolve("Darwin").resolve("x86_64").resolve("bin").resolve("z3").toString()
     } else {
-      tool_home.resolve("z3").resolve("4.3.2").resolve("Linux").resolve("x86_64").resolve("bin").resolve("z3").toString()
+      tool_home.resolve("z3").resolve("4.3.1").resolve("Linux").resolve("x86_64").resolve("bin").resolve("z3").toString()
     }
     val boogie_exe=if(OS.startsWith("Windows")){
       tool_home.resolve("boogie").resolve("2012-10-22").resolve("windows").resolve("bin").resolve("boogie").toString()
     } else {
       tool_home.resolve("boogie").resolve("2012-10-22").resolve("unix").resolve("bin").resolve("boogie").toString()
     }
     val carbon = new viper.carbon.CarbonVerifier(Seq("startedBy" -> "example", "fullCmd" -> "dummy"))
+    print(Seq(
+        "--z3Exe",z3_exe,
+        "--boogieExe",boogie_exe,
+        "-"));
     carbon.parseCommandLine(Seq(
         "--z3Exe",z3_exe,
         "--boogieExe",boogie_exe,