===========================================================
                                      .___ __  __   
          _________________  __ __  __| _/|__|/  |_ 
         / ___\_` __ \__  \ |  |  \/ __ | | \\_  __\
        / /_/  >  | \// __ \|  |  / /_/ | |  ||  |  
        \___  /|__|  (____  /____/\____ | |__||__|  
       /_____/            \/           \/           
              grep rough audit - static analysis tool
                  v2.8 written by @Wireghoul
=================================[justanotherhacker.com]===
cvc4-1.8/cmake/CVC4Config.cmake.in-6-if(NOT TARGET CVC4::cvc4)
cvc4-1.8/cmake/CVC4Config.cmake.in:7:  include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake)
cvc4-1.8/cmake/CVC4Config.cmake.in-8-endif()
##############################################
cvc4-1.8/cmake/CVC4Config.cmake.in-11-  set_and_check(CVC4_JNI_PATH "@PACKAGE_LIBRARY_INSTALL_DIR@")
cvc4-1.8/cmake/CVC4Config.cmake.in:12:  include(${CMAKE_CURRENT_LIST_DIR}/CVC4JavaTargets.cmake)
cvc4-1.8/cmake/CVC4Config.cmake.in-13-endif()
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc26-fnt-2-
cvc4-1.8/contrib/competitions/casc/run-script-casc26-fnt:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc26-fnt-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc26-fof-4-
cvc4-1.8/contrib/competitions/casc/run-script-casc26-fof:5:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc26-fof-6-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc26-tfa-2-
cvc4-1.8/contrib/competitions/casc/run-script-casc26-tfa:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc26-tfa-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc27-fnt-2-
cvc4-1.8/contrib/competitions/casc/run-script-casc27-fnt:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc27-fnt-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc27-fof-4-
cvc4-1.8/contrib/competitions/casc/run-script-casc27-fof:5:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc27-fof-6-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc27-tfa-2-
cvc4-1.8/contrib/competitions/casc/run-script-casc27-tfa:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc27-tfa-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc27-tfn-nr-2-
cvc4-1.8/contrib/competitions/casc/run-script-casc27-tfn-nr:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc27-tfn-nr-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc27-thf-4-
cvc4-1.8/contrib/competitions/casc/run-script-casc27-thf:5:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc27-thf-6-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-casc27-thf-sat-nr-2-
cvc4-1.8/contrib/competitions/casc/run-script-casc27-thf-sat-nr:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-casc27-thf-sat-nr-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-fnt-2-
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-fnt:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-fnt-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-fof-2-
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-fof:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-fof-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-tfa-2-
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-tfa:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-tfa-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-tfn-2-
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-tfn:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-cascj8-tfn-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-fnt-2-
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-fnt:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-fnt-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-fof-4-
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-fof:5:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-fof-6-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-tfa-2-
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-tfa:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-tfa-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-tfn-nr-2-
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-tfn-nr:3:here=`dirname $0`
cvc4-1.8/contrib/competitions/casc/run-script-cascj9-tfn-nr-4-cvc4=$here/cvc4
##############################################
cvc4-1.8/contrib/cut-release-11-version=""
cvc4-1.8/contrib/cut-release:12:cutrelease=`basename "$0"`
cvc4-1.8/contrib/cut-release-13-
##############################################
cvc4-1.8/contrib/cut-release-137-echo "Checking whether release \`$version' already exists..."
cvc4-1.8/contrib/cut-release:138:if [ -n "`git tag -l "$version"`" ]; then
cvc4-1.8/contrib/cut-release-139-  error "Git repo already contains a release \`$version'"
##############################################
cvc4-1.8/contrib/debug-keys-7-if [ "$1" = "-h" -o "$1" = "-help" -o "$1" = "-?" -o "$1" = "--help" ]; then
cvc4-1.8/contrib/debug-keys:8:  echo "usage: `basename $0` [dirs...]" >&2
cvc4-1.8/contrib/debug-keys-9-  echo "This utility will print all Debug("foo") and Trace("foo") keys."
##############################################
cvc4-1.8/contrib/debug-keys-14-if [ $# -eq 0 ]; then
cvc4-1.8/contrib/debug-keys:15:  cd `dirname "$0"`/..
cvc4-1.8/contrib/debug-keys-16-
cvc4-1.8/contrib/debug-keys-17-  if ! [ -d src ]; then
cvc4-1.8/contrib/debug-keys:18:    echo "`basename $0`: not in CVC4 directory tree?!" >&2
cvc4-1.8/contrib/debug-keys-19-    exit 1
##############################################
cvc4-1.8/contrib/depgraph-8-
cvc4-1.8/contrib/depgraph:9:progname=`basename "$0"`
cvc4-1.8/contrib/depgraph-10-
##############################################
cvc4-1.8/contrib/depgraph-33-
cvc4-1.8/contrib/depgraph:34:cd "`dirname \"$0\"`/.."
cvc4-1.8/contrib/depgraph-35-
##############################################
cvc4-1.8/contrib/depgraph-62-  for path in $paths; do
cvc4-1.8/contrib/depgraph:63:    dir=`echo "$path" | sed 's,^\([^/]*\).*,\1,'`
cvc4-1.8/contrib/depgraph:64:    file=`echo "$path" | sed 's,^[^/]*/,,'`
cvc4-1.8/contrib/depgraph:65:    package=`echo "$file" | sed 's,^\(.*\)/.*,\1,'`
cvc4-1.8/contrib/depgraph:66:    file=`echo "$file" | sed 's,^.*/,,'`
cvc4-1.8/contrib/depgraph-67-    if [ -n "$target" -a "$target" != "$package" ]; then continue; fi
##############################################
cvc4-1.8/contrib/depgraph-82-for path in $paths; do
cvc4-1.8/contrib/depgraph:83:    dir=`echo "$path" | sed 's,^\([^/]*\).*,\1,'`
cvc4-1.8/contrib/depgraph:84:    file=`echo "$path" | sed 's,^[^/]*/,,'`
cvc4-1.8/contrib/depgraph:85:    package=`echo "$file" | sed 's,^\(.*\)/.*,\1,'`
cvc4-1.8/contrib/depgraph:86:    file=`echo "$file" | sed 's,^.*/,,'`
cvc4-1.8/contrib/depgraph:87:    incs=`grep '^# *include *".*"' "$path" | sed 's,^# *include *"\(.*\)".*,\1,'`
cvc4-1.8/contrib/depgraph-88-    if [ -n "$target" -a "$target" != "$package" ]; then continue; fi
##############################################
cvc4-1.8/contrib/depgraph-100-      incpath=
cvc4-1.8/contrib/depgraph:101:      dirpackageparent="$dir/`dirname "$package"`"
cvc4-1.8/contrib/depgraph-102-      for incdir in "$dir" "$dir/include" "$dir/$package" . "$dirpackageparent"; do
##############################################
cvc4-1.8/contrib/depgraph-108-      fi
cvc4-1.8/contrib/depgraph:109:      incpath=`echo "$incpath" | sed 's,^\./,,'`
cvc4-1.8/contrib/depgraph:110:      incpath=`echo "$incpath" | sed "s,^$dir/,,"`
cvc4-1.8/contrib/depgraph:111:      incdir=`echo "$incpath" | sed 's,^\([^/]*\).*,\1,'`
cvc4-1.8/contrib/depgraph:112:      incpackage=`echo "$incpath" | sed 's,^\(.*\)/.*,\1,'`
cvc4-1.8/contrib/depgraph:113:      incfile=`echo "$incpath" | sed 's,^.*/,,'`
cvc4-1.8/contrib/depgraph-114-      if [ "$mode" = packages ]; then
##############################################
cvc4-1.8/contrib/get-win-dependencies-107-echo 'Now just run:'
cvc4-1.8/contrib/get-win-dependencies:108:echo "  ./configure --enable-static-binary --disable-shared --host=$HOST LDFLAGS=\"-L`pwd`/gmp-$GMPVERSION/lib -L`pwd`/antlr-3.4/lib -L`pwd`/boost-$BOOSTVERSION/lib\" CPPFLAGS=\"-I`pwd`/gmp-$GMPVERSION/include -I`pwd`/antlr-3.4/include -I`pwd`/boost-$BOOSTVERSION/include\" --with-antlr-dir=\"`pwd`/antlr-3.4\" ANTLR=\"`pwd`/antlr-3.4/bin/antlr3\""
cvc4-1.8/contrib/get-win-dependencies-109-echo '  make'
##############################################
cvc4-1.8/contrib/new-theory-5-
cvc4-1.8/contrib/new-theory:6:cd "`dirname "$0"`/.."
cvc4-1.8/contrib/new-theory-7-
##############################################
cvc4-1.8/contrib/new-theory-93-
cvc4-1.8/contrib/new-theory:94:id="`echo "$dir" | tr a-z A-Z`"
cvc4-1.8/contrib/new-theory-95-# convoluted, but should be relatively portable and give a CamelCase
cvc4-1.8/contrib/new-theory-96-# representation for a string.  (e.g. "foo_bar" becomes "FooBar")
cvc4-1.8/contrib/new-theory:97:camel="`echo "$dir" | awk 'BEGIN { RS="_";ORS="";OFS="" } // {print toupper(substr($1,1,1)),substr($1,2,length($1))} END {print "\n"}'`"
cvc4-1.8/contrib/new-theory-98-
##############################################
cvc4-1.8/contrib/new-theory-112-  src="$1"
cvc4-1.8/contrib/new-theory:113:  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
cvc4-1.8/contrib/new-theory-114-  echo "Creating src/theory/$dir/$dest..."
##############################################
cvc4-1.8/contrib/new-theory-121-  src="$1"
cvc4-1.8/contrib/new-theory:122:  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
cvc4-1.8/contrib/new-theory-123-  echo "Creating src/theory/$dir/$dest..."
##############################################
cvc4-1.8/contrib/new-theory-130-  src="$1"
cvc4-1.8/contrib/new-theory:131:  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
cvc4-1.8/contrib/new-theory-132-  echo "Creating src/options/$dest..."
##############################################
cvc4-1.8/contrib/update-copyright.pl-140-  return if ($srcdir.'/'.$file) =~ /$excluded_paths/;
cvc4-1.8/contrib/update-copyright.pl:141:  return if $modonly && `git status -s "$srcdir/$file" 2>/dev/null` !~ /^(M|.M)/;
cvc4-1.8/contrib/update-copyright.pl-142-  print "$srcdir/$file...";
##############################################
cvc4-1.8/contrib/update-copyright.pl-230-  close $OUT;
cvc4-1.8/contrib/update-copyright.pl:231:  rename($outfile, $infile) || die "can't rename working file \`$outfile' to \`$infile'";
cvc4-1.8/contrib/update-copyright.pl-232-}
##############################################
cvc4-1.8/src/base/mktagheaders-19-echo 'static char const* const '$TAG_NAME'[] = {';
cvc4-1.8/src/base/mktagheaders:20:for tag in `cat $TAG_FILE`; do
cvc4-1.8/src/base/mktagheaders-21-  echo "\"$tag\",";
##############################################
cvc4-1.8/src/bindings/CMakeLists.txt-18-
cvc4-1.8/src/bindings/CMakeLists.txt:19:include(${SWIG_USE_FILE})
cvc4-1.8/src/bindings/CMakeLists.txt-20-
##############################################
cvc4-1.8/src/expr/mkexpr-19-
cvc4-1.8/src/expr/mkexpr:20:filename=`basename "$1" | sed 's,_template,,'`
cvc4-1.8/src/expr/mkexpr-21-template_rel="<CVC4>/"$(realpath --relative-to $CMAKE_SOURCE_DIR $1)
##############################################
cvc4-1.8/src/expr/mkexpr-308-done
cvc4-1.8/src/expr/mkexpr:309:error=`expr "$text" : '.*\${\([^}]*\)}.*'`
cvc4-1.8/src/expr/mkexpr-310-if [ -n "$error" ]; then
##############################################
cvc4-1.8/src/expr/mkkind-18-
cvc4-1.8/src/expr/mkkind:19:filename=`basename "$1" | sed 's,_template,,'`
cvc4-1.8/src/expr/mkkind-20-template_rel="<CVC4>/"$(realpath --relative-to $CMAKE_SOURCE_DIR $1)
##############################################
cvc4-1.8/src/expr/mkkind-414-done
cvc4-1.8/src/expr/mkkind:415:error=`expr "$text" : '.*\${\([^}]*\)}.*'`
cvc4-1.8/src/expr/mkkind-416-if [ -n "$error" ]; then
##############################################
cvc4-1.8/src/expr/mkmetakind-279-"
cvc4-1.8/src/expr/mkmetakind:280:  cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'`
cvc4-1.8/src/expr/mkmetakind-281-  metakind_constDeleters="${metakind_constDeleters}
##############################################
cvc4-1.8/src/expr/mkmetakind-318-  elif expr "$nc" : '[0-9][0-9]*:$' >/dev/null; then
cvc4-1.8/src/expr/mkmetakind:319:    let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
cvc4-1.8/src/expr/mkmetakind-320-    ub="expr::NodeValue::MAX_CHILDREN"
cvc4-1.8/src/expr/mkmetakind-321-  elif expr "$nc" : '[0-9][0-9]*:[0-9][0-9]*$' >/dev/null; then
cvc4-1.8/src/expr/mkmetakind:322:    let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
cvc4-1.8/src/expr/mkmetakind-323-    if [ $ub -lt $lb ]; then
##############################################
cvc4-1.8/src/expr/mkmetakind-341-function primitive_type {
cvc4-1.8/src/expr/mkmetakind:342:  strip=`expr "$1" : ' *\(.*\)\* *'`
cvc4-1.8/src/expr/mkmetakind-343-  if [ -n "$strip" ]; then
##############################################
cvc4-1.8/src/expr/mkmetakind-419-done
cvc4-1.8/src/expr/mkmetakind:420:error=`expr "$text" : '.*\${\([^}]*\)}.*'`
cvc4-1.8/src/expr/mkmetakind-421-if [ -n "$error" ]; then
##############################################
cvc4-1.8/src/theory/mkrewriter-262-done
cvc4-1.8/src/theory/mkrewriter:263:error=`expr "$text" : '.*\${\([^}]*\)}.*'`
cvc4-1.8/src/theory/mkrewriter-264-if [ -n "$error" ]; then
##############################################
cvc4-1.8/src/theory/mktheorytraits-18-
cvc4-1.8/src/theory/mktheorytraits:19:filename=`basename "$1" | sed 's,_template,,'`
cvc4-1.8/src/theory/mktheorytraits-20-
##############################################
cvc4-1.8/src/theory/mktheorytraits-413-done
cvc4-1.8/src/theory/mktheorytraits:414:error=`expr "$text" : '.*\${\([^}]*\)}.*'`
cvc4-1.8/src/theory/mktheorytraits-415-if [ -n "$error" ]; then
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-86-(declare-fun type_pointer (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:87:(declare-fun type_addr (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-88-(declare-fun type_alloc_table () c_type)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-89-(declare-fun block_length (c_ssorted c_ssorted) Int)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:90:(declare-fun base_addr (c_ssorted) c_unique)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-91-(declare-fun offset (c_ssorted) Int)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-110-(assert (forall ((?t_12_122_70 c_type)) (forall ((?p_121_71 c_unique)) (forall ((?i_120_72 Int)) (forall ((?j_119_73 Int)) (let ((?v_0 (type_pointer ?t_12_122_70))) (let ((?v_1 (c_sort ?v_0 ?p_121_71))) (= (shift (c_sort ?v_0 (shift ?v_1 ?i_120_72)) ?j_119_73) (shift ?v_1 (+ ?i_120_72 ?j_119_73))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:111:(assert (forall ((?t_13_125_74 c_type)) (forall ((?p_124_75 c_unique)) (forall ((?i_123_76 Int)) (let ((?v_0 (type_pointer ?t_13_125_74))) (let ((?v_1 (c_sort ?v_0 ?p_124_75))) (= (base_addr (c_sort ?v_0 (shift ?v_1 ?i_123_76))) (base_addr ?v_1))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-112-(assert (forall ((?t_14_129_77 c_type)) (forall ((?a_128_78 c_unique)) (forall ((?p_127_79 c_unique)) (forall ((?i_126_80 Int)) (let ((?v_1 (c_sort type_alloc_table ?a_128_78)) (?v_0 (type_pointer ?t_14_129_77))) (let ((?v_2 (c_sort ?v_0 ?p_127_79))) (= (block_length ?v_1 (c_sort ?v_0 (shift ?v_2 ?i_126_80))) (block_length ?v_1 ?v_2)))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-154-(assert (forall ((?t_42_259_176 c_type)) (forall ((?t_41_258_177 c_type)) (forall ((?l_257_178 c_unique)) (forall ((?m_256_179 c_unique)) (forall ((?p_255_180 c_unique)) (let ((?v_0 (type_pointer ?t_42_259_176))) (=> (not_in_pset (c_sort ?v_0 ?p_255_180) (c_sort (type_pset ?t_42_259_176) (pset_star (c_sort (type_pset ?t_41_258_177) ?l_257_178) (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179)))) (forall ((?p1_254_181 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_41_258_177) ?p1_254_181))) (=> (= ?p_255_180 (acc (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_41_258_177) ?l_257_178)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:155:(assert (forall ((?t_43_263_182 c_type)) (forall ((?p_262_183 c_unique)) (forall ((?l_261_184 c_unique)) (let ((?v_0 (type_pset ?t_43_263_182))) (=> (forall ((?p1_260_185 c_unique)) (let ((?v_1 (type_pointer ?t_43_263_182))) (let ((?v_2 (c_sort ?v_1 ?p1_260_185))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_261_184))) (not (= (base_addr (c_sort ?v_1 ?p_262_183)) (base_addr ?v_2))))))) (not_in_pset (c_sort (type_pointer ?t_43_263_182) ?p_262_183) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_261_184))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:156:(assert (forall ((?t_44_267_186 c_type)) (forall ((?p_266_187 c_unique)) (forall ((?l_265_188 c_unique)) (let ((?v_0 (type_pset ?t_44_267_186))) (=> (not_in_pset (c_sort (type_pointer ?t_44_267_186) ?p_266_187) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_265_188)))) (forall ((?p1_264_189 c_unique)) (let ((?v_1 (type_pointer ?t_44_267_186))) (let ((?v_2 (c_sort ?v_1 ?p1_264_189))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_265_188))) (not (= (base_addr (c_sort ?v_1 ?p_266_187)) (base_addr ?v_2)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-157-(assert (forall ((?t_45_274_190 c_type)) (forall ((?p_273_191 c_unique)) (forall ((?l_272_192 c_unique)) (forall ((?a_271_193 Int)) (forall ((?b_270_194 Int)) (let ((?v_0 (type_pset ?t_45_274_190))) (=> (forall ((?p1_269_195 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) (c_sort ?v_0 ?l_272_192)) (forall ((?i_268_196 Int)) (=> (and (<= ?a_271_193 ?i_268_196) (<= ?i_268_196 ?b_270_194)) (not (= ?p_273_191 (shift (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) ?i_268_196))))))) (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p_273_191) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_272_192) ?a_271_193 ?b_270_194)))))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-178-(declare-fun separation1 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:179:(assert (forall ((?t_78_404_321 c_type)) (forall ((?t_77_403_322 c_type)) (forall ((?m1_402_323 c_unique)) (forall ((?m2_401_324 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_77_403_322) ?t_78_404_321))) (= (separation1 (c_sort ?v_0 ?m1_402_323) (c_sort ?v_0 ?m2_401_324)) (forall ((?p_400_325 c_unique)) (forall ((?a_399_326 c_unique)) (let ((?v_1 (type_pointer ?t_77_403_322)) (?v_2 (c_sort (type_pointer ?t_78_404_321) ?p_400_325))) (=> (valid (c_sort type_alloc_table ?a_399_326) ?v_2) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_402_323) ?v_2))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_401_324) ?v_2))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-180-(declare-fun separation1_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:181:(assert (forall ((?t_80_412_327 c_type)) (forall ((?t_79_411_328 c_type)) (forall ((?m1_410_329 c_unique)) (forall ((?m2_409_330 c_unique)) (forall ((?size_408_331 Int)) (let ((?v_0 (type_memory (type_pointer ?t_79_411_328) ?t_80_412_327))) (= (separation1_range1 (c_sort ?v_0 ?m1_410_329) (c_sort ?v_0 ?m2_409_330) ?size_408_331) (forall ((?p_407_332 c_unique)) (forall ((?a_406_333 c_unique)) (=> (valid (c_sort type_alloc_table ?a_406_333) (c_sort (type_pointer ?t_80_412_327) ?p_407_332)) (forall ((?i_405_334 Int)) (let ((?v_1 (type_pointer ?t_79_411_328)) (?v_2 (type_pointer ?t_80_412_327))) (let ((?v_3 (c_sort ?v_2 ?p_407_332))) (=> (and (<= 0 ?i_405_334) (< ?i_405_334 ?size_408_331)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_410_329) (c_sort ?v_2 (shift ?v_3 ?i_405_334))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_409_330) ?v_3))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-182-(declare-fun separation1_range (c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:183:(assert (forall ((?t_82_420_335 c_type)) (forall ((?t_81_419_336 c_type)) (forall ((?m_418_337 c_unique)) (forall ((?size_417_338 Int)) (= (separation1_range (c_sort (type_memory (type_pointer ?t_81_419_336) ?t_82_420_335) ?m_418_337) ?size_417_338) (forall ((?p_416_339 c_unique)) (forall ((?a_415_340 c_unique)) (=> (valid (c_sort type_alloc_table ?a_415_340) (c_sort (type_pointer ?t_82_420_335) ?p_416_339)) (forall ((?i1_414_341 Int)) (forall ((?i2_413_342 Int)) (let ((?v_0 (type_pointer ?t_81_419_336))) (let ((?v_2 (c_sort (type_memory ?v_0 ?t_82_420_335) ?m_418_337)) (?v_1 (type_pointer ?t_82_420_335))) (let ((?v_3 (c_sort ?v_1 ?p_416_339))) (=> (and (<= 0 ?i1_414_341) (< ?i1_414_341 ?size_417_338)) (=> (and (<= 0 ?i2_413_342) (< ?i2_413_342 ?size_417_338)) (=> (not (= ?i1_414_341 ?i2_413_342)) (not (= (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i1_414_341))))) (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i2_413_342))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-184-(declare-fun separation2 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:185:(assert (forall ((?t_84_426_343 c_type)) (forall ((?t_83_425_344 c_type)) (forall ((?m1_424_345 c_unique)) (forall ((?m2_423_346 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_83_425_344) ?t_84_426_343))) (= (separation2 (c_sort ?v_0 ?m1_424_345) (c_sort ?v_0 ?m2_423_346)) (forall ((?p1_422_347 c_unique)) (forall ((?p2_421_348 c_unique)) (let ((?v_1 (type_pointer ?t_83_425_344)) (?v_2 (type_pointer ?t_84_426_343))) (=> (not (= ?p1_422_347 ?p2_421_348)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_424_345) (c_sort ?v_2 ?p1_422_347)))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_423_346) (c_sort ?v_2 ?p2_421_348)))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-186-(declare-fun separation2_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:187:(assert (forall ((?t_86_435_349 c_type)) (forall ((?t_85_434_350 c_type)) (forall ((?m1_433_351 c_unique)) (forall ((?m2_432_352 c_unique)) (forall ((?size_431_353 Int)) (let ((?v_0 (type_memory (type_pointer ?t_85_434_350) ?t_86_435_349))) (= (separation2_range1 (c_sort ?v_0 ?m1_433_351) (c_sort ?v_0 ?m2_432_352) ?size_431_353) (forall ((?p_430_354 c_unique)) (forall ((?q_429_355 c_unique)) (forall ((?a_428_356 c_unique)) (forall ((?i_427_357 Int)) (let ((?v_1 (type_pointer ?t_85_434_350)) (?v_2 (type_pointer ?t_86_435_349))) (=> (and (<= 0 ?i_427_357) (< ?i_427_357 ?size_431_353)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_433_351) (c_sort ?v_2 (shift (c_sort ?v_2 ?p_430_354) ?i_427_357))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_432_352) (c_sort ?v_2 ?q_429_355))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-188-(declare-fun on_heap (c_ssorted c_ssorted) Bool)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-205-(declare-fun separation_anonymous_0_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:206:(assert (forall ((?x_global_489_396 c_unique)) (forall ((?anonymous_0PM_global_488_397 c_unique)) (forall ((?tab_487_398 c_unique)) (forall ((?v_486_399 c_unique)) (forall ((?alloc_485_400 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global)) (?v_2 (c_sort ?v_1 ?tab_487_398)) (?v_3 (c_sort ?v_1 ?v_486_399))) (= (separation_anonymous_0_int (c_sort ?v_0 ?x_global_489_396) (c_sort ?v_0 ?anonymous_0PM_global_488_397) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_485_400)) (and (not (= (base_addr ?v_2) (base_addr ?v_3))) (forall ((?index_3_484_401 Int)) (=> (and (<= 0 ?index_3_484_401) (< ?index_3_484_401 5)) (not (= (base_addr ?v_3) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_489_396) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_488_397) (c_sort ?v_1 (shift ?v_2 ?index_3_484_401)))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-207-(declare-fun separation_anonymous_0_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:208:(assert (forall ((?x_global_498_402 c_unique)) (forall ((?u_global_497_403 c_unique)) (forall ((?t_global_496_404 c_unique)) (forall ((?s1PM_global_495_405 c_unique)) (forall ((?anonymous_0PM_global_494_406 c_unique)) (forall ((?tab_493_407 c_unique)) (forall ((?s_492_408 c_unique)) (forall ((?alloc_491_409 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_497_403)) (?v_5 (c_sort ?v_0 ?t_global_496_404)) (?v_6 (c_sort ?v_0 ?s1PM_global_495_405)) (?v_2 (c_sort ?v_1 ?tab_493_407)) (?v_3 (c_sort ?v_1 ?s_492_408))) (let ((?v_4 (base_addr ?v_2)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_0_s1 (c_sort ?v_0 ?x_global_498_402) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_494_406) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_491_409)) (and (not (= ?v_4 (base_addr ?v_3))) (and (forall ((?index_6_490_410 Int)) (=> (and (<= 0 ?index_6_490_410) (< ?index_6_490_410 5)) (not (= (base_addr ?v_3) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_498_402) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_494_406) (c_sort ?v_1 (shift ?v_2 ?index_6_490_410))))))))))) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-209-(declare-fun separation_anonymous_1_anonymous_0 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:210:(assert (forall ((?x_global_507_411 c_unique)) (forall ((?p2_global_506_412 c_unique)) (forall ((?p1_global_505_413 c_unique)) (forall ((?anonymous_1PM_global_504_414 c_unique)) (forall ((?anonymous_0PM_global_503_415 c_unique)) (forall ((?u1_502_416 c_unique)) (forall ((?tab_501_417 c_unique)) (forall ((?alloc_500_418 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_506_412)) (?v_5 (c_sort ?v_0 ?p1_global_505_413)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_504_414)) (?v_2 (c_sort ?v_1 ?u1_502_416)) (?v_3 (c_sort ?v_1 ?tab_501_417))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_1_anonymous_0 (c_sort ?v_0 ?x_global_507_411) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_503_415) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_500_418)) (and (not (= (base_addr ?v_2) ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (forall ((?index_7_499_419 Int)) (=> (and (<= 0 ?index_7_499_419) (< ?index_7_499_419 5)) (not (= (base_addr ?v_2) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_507_411) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_503_415) (c_sort ?v_1 (shift ?v_3 ?index_7_499_419)))))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-211-(declare-fun separation_anonymous_1_anonymous_1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:212:(assert (forall ((?p2_global_513_420 c_unique)) (forall ((?p1_global_512_421 c_unique)) (forall ((?anonymous_1PM_global_511_422 c_unique)) (forall ((?u2_510_423 c_unique)) (forall ((?u1_509_424 c_unique)) (forall ((?alloc_508_425 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_513_420)) (?v_5 (c_sort ?v_0 ?p1_global_512_421)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_511_422)) (?v_2 (c_sort ?v_1 ?u2_510_423)) (?v_3 (c_sort ?v_1 ?u1_509_424))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_1_anonymous_1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_508_425)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-213-(declare-fun separation_anonymous_1_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:214:(assert (forall ((?p2_global_519_426 c_unique)) (forall ((?p1_global_518_427 c_unique)) (forall ((?anonymous_1PM_global_517_428 c_unique)) (forall ((?u1_516_429 c_unique)) (forall ((?v_515_430 c_unique)) (forall ((?alloc_514_431 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_519_426)) (?v_5 (c_sort ?v_0 ?p1_global_518_427)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_517_428)) (?v_2 (c_sort ?v_1 ?u1_516_429)) (?v_3 (c_sort ?v_1 ?v_515_430))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_1_int ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_514_431)) (and (not (= (base_addr ?v_2) ?v_4)) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-215-(declare-fun separation_anonymous_1_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:216:(assert (forall ((?u_global_528_432 c_unique)) (forall ((?t_global_527_433 c_unique)) (forall ((?s1PM_global_526_434 c_unique)) (forall ((?p2_global_525_435 c_unique)) (forall ((?p1_global_524_436 c_unique)) (forall ((?anonymous_1PM_global_523_437 c_unique)) (forall ((?u1_522_438 c_unique)) (forall ((?s_521_439 c_unique)) (forall ((?alloc_520_440 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?u_global_528_432)) (?v_10 (c_sort ?v_0 ?t_global_527_433)) (?v_11 (c_sort ?v_0 ?s1PM_global_526_434)) (?v_7 (c_sort ?v_0 ?p2_global_525_435)) (?v_5 (c_sort ?v_0 ?p1_global_524_436)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_523_437)) (?v_2 (c_sort ?v_1 ?u1_522_438)) (?v_3 (c_sort ?v_1 ?s_521_439))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_1_s1 ?v_12 ?v_10 ?v_11 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_520_440)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-217-(declare-fun separation_anonymous_2_anonymous_0 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:218:(assert (forall ((?x_global_537_441 c_unique)) (forall ((?anonymous_2_p2_global_536_442 c_unique)) (forall ((?anonymous_2_p1_global_535_443 c_unique)) (forall ((?anonymous_2PM_global_534_444 c_unique)) (forall ((?anonymous_0PM_global_533_445 c_unique)) (forall ((?u3_532_446 c_unique)) (forall ((?tab_531_447 c_unique)) (forall ((?alloc_530_448 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_536_442)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_535_443)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_534_444)) (?v_2 (c_sort ?v_1 ?u3_532_446)) (?v_3 (c_sort ?v_1 ?tab_531_447))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_2_anonymous_0 (c_sort ?v_0 ?x_global_537_441) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_533_445) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_530_448)) (and (not (= (base_addr ?v_2) ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (forall ((?index_15_529_449 Int)) (=> (and (<= 0 ?index_15_529_449) (< ?index_15_529_449 5)) (not (= (base_addr ?v_2) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_537_441) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_533_445) (c_sort ?v_1 (shift ?v_3 ?index_15_529_449)))))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-219-(declare-fun separation_anonymous_2_anonymous_1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:220:(assert (forall ((?p2_global_546_450 c_unique)) (forall ((?p1_global_545_451 c_unique)) (forall ((?anonymous_2_p2_global_544_452 c_unique)) (forall ((?anonymous_2_p1_global_543_453 c_unique)) (forall ((?anonymous_2PM_global_542_454 c_unique)) (forall ((?anonymous_1PM_global_541_455 c_unique)) (forall ((?u3_540_456 c_unique)) (forall ((?u1_539_457 c_unique)) (forall ((?alloc_538_458 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?p2_global_546_450)) (?v_10 (c_sort ?v_0 ?p1_global_545_451)) (?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_544_452)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_543_453)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_542_454)) (?v_11 (c_sort ?v_0 ?anonymous_1PM_global_541_455)) (?v_2 (c_sort ?v_1 ?u3_540_456)) (?v_3 (c_sort ?v_1 ?u1_539_457))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_2_anonymous_1 ?v_12 ?v_10 ?v_7 ?v_5 ?v_6 ?v_11 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_538_458)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-221-(declare-fun separation_anonymous_2_anonymous_2 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:222:(assert (forall ((?anonymous_2_p2_global_552_459 c_unique)) (forall ((?anonymous_2_p1_global_551_460 c_unique)) (forall ((?anonymous_2PM_global_550_461 c_unique)) (forall ((?u4_549_462 c_unique)) (forall ((?u3_548_463 c_unique)) (forall ((?alloc_547_464 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_552_459)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_551_460)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_550_461)) (?v_2 (c_sort ?v_1 ?u4_549_462)) (?v_3 (c_sort ?v_1 ?u3_548_463))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_2_anonymous_2 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_547_464)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-223-(declare-fun separation_anonymous_2_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:224:(assert (forall ((?anonymous_2_p2_global_558_465 c_unique)) (forall ((?anonymous_2_p1_global_557_466 c_unique)) (forall ((?anonymous_2PM_global_556_467 c_unique)) (forall ((?u3_555_468 c_unique)) (forall ((?v_554_469 c_unique)) (forall ((?alloc_553_470 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_558_465)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_557_466)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_556_467)) (?v_2 (c_sort ?v_1 ?u3_555_468)) (?v_3 (c_sort ?v_1 ?v_554_469))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_2_int ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_553_470)) (and (not (= (base_addr ?v_2) ?v_4)) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-225-(declare-fun separation_anonymous_2_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:226:(assert (forall ((?u_global_567_471 c_unique)) (forall ((?t_global_566_472 c_unique)) (forall ((?s1PM_global_565_473 c_unique)) (forall ((?anonymous_2_p2_global_564_474 c_unique)) (forall ((?anonymous_2_p1_global_563_475 c_unique)) (forall ((?anonymous_2PM_global_562_476 c_unique)) (forall ((?u3_561_477 c_unique)) (forall ((?s_560_478 c_unique)) (forall ((?alloc_559_479 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?u_global_567_471)) (?v_10 (c_sort ?v_0 ?t_global_566_472)) (?v_11 (c_sort ?v_0 ?s1PM_global_565_473)) (?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_564_474)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_563_475)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_562_476)) (?v_2 (c_sort ?v_1 ?u3_561_477)) (?v_3 (c_sort ?v_1 ?s_560_478))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_2_s1 ?v_12 ?v_10 ?v_11 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_559_479)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-227-(declare-fun separation_int_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:228:(assert (forall ((?u_global_573_480 c_unique)) (forall ((?t_global_572_481 c_unique)) (forall ((?s1PM_global_571_482 c_unique)) (forall ((?v_570_483 c_unique)) (forall ((?s_569_484 c_unique)) (forall ((?alloc_568_485 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_573_480)) (?v_5 (c_sort ?v_0 ?t_global_572_481)) (?v_6 (c_sort ?v_0 ?s1PM_global_571_482)) (?v_2 (c_sort ?v_1 ?v_570_483)) (?v_3 (c_sort ?v_1 ?s_569_484))) (let ((?v_4 (base_addr ?v_2)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_int_s1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_568_485)) (and (not (= ?v_4 (base_addr ?v_3))) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-229-(declare-fun separation_s1_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:230:(assert (forall ((?u_global_579_486 c_unique)) (forall ((?t_global_578_487 c_unique)) (forall ((?s1PM_global_577_488 c_unique)) (forall ((?ss_576_489 c_unique)) (forall ((?s_575_490 c_unique)) (forall ((?alloc_574_491 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_579_486)) (?v_5 (c_sort ?v_0 ?t_global_578_487)) (?v_6 (c_sort ?v_0 ?s1PM_global_577_488)) (?v_2 (c_sort ?v_1 ?ss_576_489)) (?v_3 (c_sort ?v_1 ?s_575_490))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_s1_s1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_574_491)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2:231:(assert (not (forall ((?alloc c_unique)) (forall ((?anonymous_2PM_global c_unique)) (forall ((?anonymous_2_p1_global c_unique)) (forall ((?anonymous_2_p2_global c_unique)) (forall ((?anonymous_2_v1_global c_unique)) (forall ((?anonymous_2_v2_global c_unique)) (forall ((?intM_global c_unique)) (forall ((?u3 c_unique)) (forall ((?u4 c_unique)) (forall ((?w1 c_unique)) (forall ((?w10 c_unique)) (forall ((?w2 c_unique)) (forall ((?w3 c_unique)) (forall ((?w4 c_unique)) (forall ((?w5 c_unique)) (forall ((?w6 c_unique)) (forall ((?w7 c_unique)) (forall ((?w8 c_unique)) (forall ((?w9 c_unique)) (let ((?v_0 (type_pointer type_global))) (let ((?v_2 (type_memory ?v_0 type_global)) (?v_3 (c_sort ?v_0 ?w3))) (let ((?v_5 (base_addr ?v_3)) (?v_8 (c_sort ?v_0 ?u4))) (let ((?v_1 (base_addr ?v_8)) (?v_6 (c_sort ?v_2 ?anonymous_2_p1_global)) (?v_7 (c_sort ?v_2 ?anonymous_2PM_global))) (let ((?v_4 (c_sort ?v_0 (acc ?v_7 ?v_3)))) (let ((?v_12 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_4)))) (?v_9 (c_sort ?v_2 ?anonymous_2_p2_global))) (let ((?v_13 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_4)))) (?v_10 (c_sort ?v_0 (acc ?v_7 ?v_8)))) (let ((?v_16 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_10)))) (?v_17 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_10)))) (?v_14 (c_sort ?v_0 ?u3))) (let ((?v_11 (base_addr ?v_14)) (?v_15 (c_sort ?v_0 (acc ?v_7 ?v_14)))) (let ((?v_18 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_15)))) (?v_19 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_15)))) (?v_20 (c_sort ?v_0 ?w1))) (let ((?v_22 (base_addr ?v_20)) (?v_21 (c_sort ?v_0 (acc ?v_7 ?v_20)))) (let ((?v_23 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_21)))) (?v_24 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_21)))) (?v_25 (c_sort type_alloc_table ?alloc)) (?v_54 (c_sort ?v_0 ?w9)) (?v_26 (c_sort ?v_0 ?w8)) (?v_27 (c_sort ?v_0 ?w7)) (?v_32 (c_sort ?v_0 ?w6)) (?v_37 (c_sort ?v_0 ?w5)) (?v_40 (c_sort ?v_0 ?w4)) (?v_43 (c_sort ?v_0 ?w2))) (let ((?v_30 (base_addr ?v_26)) (?v_28 (base_addr ?v_27)) (?v_29 (c_sort ?v_0 (acc ?v_7 ?v_26)))) (let ((?v_34 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_29)))) (?v_35 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_29)))) (?v_31 (c_sort ?v_0 (acc ?v_7 ?v_27)))) (let ((?v_59 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_31)))) (?v_60 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_31)))) (?v_33 (base_addr ?v_32)) (?v_36 (c_sort ?v_0 (acc ?v_7 ?v_32)))) (let ((?v_46 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_36)))) (?v_47 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_36)))) (?v_38 (base_addr ?v_37)) (?v_39 (c_sort ?v_0 (acc ?v_7 ?v_37)))) (let ((?v_48 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_39)))) (?v_49 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_39)))) (?v_41 (base_addr ?v_40)) (?v_42 (c_sort ?v_0 (acc ?v_7 ?v_40)))) (let ((?v_50 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_42)))) (?v_51 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_42)))) (?v_44 (base_addr ?v_43)) (?v_45 (c_sort ?v_0 (acc ?v_7 ?v_43)))) (let ((?v_52 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_45)))) (?v_53 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_45)))) (?v_66 (valid ?v_25 ?v_14)) (?v_61 (c_sort ?v_0 ?w10)) (?v_56 (base_addr ?v_54)) (?v_55 (c_sort ?v_0 (acc ?v_7 ?v_54)))) (let ((?v_57 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_55)))) (?v_58 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_55)))) (?v_63 (base_addr ?v_61)) (?v_62 (c_sort ?v_0 (acc ?v_7 ?v_61)))) (let ((?v_64 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_62)))) (?v_65 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_62))))) (=> (and (and (not (= ?v_5 ?v_1)) (and (and (not (= ?v_1 ?v_12)) (not (= ?v_1 ?v_13))) (and (not (= ?v_5 ?v_16)) (not (= ?v_5 ?v_17))))) (and (and (not (= ?v_5 ?v_11)) (and (and (not (= ?v_11 ?v_12)) (not (= ?v_11 ?v_13))) (and (not (= ?v_5 ?v_18)) (not (= ?v_5 ?v_19))))) (and (and (not (= ?v_1 ?v_11)) (and (and (not (= ?v_11 ?v_16)) (not (= ?v_11 ?v_17))) (and (not (= ?v_1 ?v_18)) (not (= ?v_1 ?v_19))))) (and (and (not (= ?v_22 ?v_1)) (and (and (not (= ?v_1 ?v_23)) (not (= ?v_1 ?v_24))) (and (not (= ?v_22 ?v_16)) (not (= ?v_22 ?v_17))))) (and (and (not (= ?v_22 ?v_11)) (and (and (not (= ?v_11 ?v_23)) (not (= ?v_11 ?v_24))) (and (not (= ?v_22 ?v_18)) (not (= ?v_22 ?v_19))))) (and (valid ?v_25 ?v_54) (and (valid ?v_25 ?v_26) (and (valid ?v_25 ?v_27) (and (valid ?v_25 ?v_32) (and (valid ?v_25 ?v_37) (and (valid ?v_25 ?v_40) (and (valid ?v_25 ?v_3) (and (valid ?v_25 ?v_43) (and (valid ?v_25 ?v_20) (and (and (not (= ?v_30 ?v_28)) (and (and (not (= ?v_28 ?v_34)) (not (= ?v_28 ?v_35))) (and (not (= ?v_30 ?v_59)) (not (= ?v_30 ?v_60))))) (and (and (not (= ?v_30 ?v_33)) (and (and (not (= ?v_33 ?v_34)) (not (= ?v_33 ?v_35))) (and (not (= ?v_30 ?v_46)) (not (= ?v_30 ?v_47))))) (and (and (not (= ?v_30 ?v_38)) (and (and (not (= ?v_38 ?v_34)) (not (= ?v_38 ?v_35))) (and (not (= ?v_30 ?v_48)) (not (= ?v_30 ?v_49))))) (and (and (not (= ?v_30 ?v_41)) (and (and (not (= ?v_41 ?v_34)) (not (= ?v_41 ?v_35))) (and (not (= ?v_30 ?v_50)) (not (= ?v_30 ?v_51))))) (and (and (not (= ?v_30 ?v_5)) (and (and (not (= ?v_5 ?v_34)) (not (= ?v_5 ?v_35))) (and (not (= ?v_30 ?v_12)) (not (= ?v_30 ?v_13))))) (and (and (not (= ?v_30 ?v_44)) (and (and (not (= ?v_44 ?v_34)) (not (= ?v_44 ?v_35))) (and (not (= ?v_30 ?v_52)) (not (= ?v_30 ?v_53))))) (and (and (not (= ?v_30 ?v_22)) (and (and (not (= ?v_22 ?v_34)) (not (= ?v_22 ?v_35))) (and (not (= ?v_30 ?v_23)) (not (= ?v_30 ?v_24))))) (and (valid ?v_25 ?v_8) (and ?v_66 (and (and (not (= ?v_33 ?v_38)) (and (and (not (= ?v_38 ?v_46)) (not (= ?v_38 ?v_47))) (and (not (= ?v_33 ?v_48)) (not (= ?v_33 ?v_49))))) (and (and (not (= ?v_33 ?v_41)) (and (and (not (= ?v_41 ?v_46)) (not (= ?v_41 ?v_47))) (and (not (= ?v_33 ?v_50)) (not (= ?v_33 ?v_51))))) (and (and (not (= ?v_33 ?v_5)) (and (and (not (= ?v_5 ?v_46)) (not (= ?v_5 ?v_47))) (and (not (= ?v_33 ?v_12)) (not (= ?v_33 ?v_13))))) (and (and (not (= ?v_33 ?v_44)) (and (and (not (= ?v_44 ?v_46)) (not (= ?v_44 ?v_47))) (and (not (= ?v_33 ?v_52)) (not (= ?v_33 ?v_53))))) (and (and (not (= ?v_33 ?v_22)) (and (and (not (= ?v_22 ?v_46)) (not (= ?v_22 ?v_47))) (and (not (= ?v_33 ?v_23)) (not (= ?v_33 ?v_24))))) (and (and (not (= ?v_30 ?v_1)) (and (and (not (= ?v_1 ?v_34)) (not (= ?v_1 ?v_35))) (and (not (= ?v_30 ?v_16)) (not (= ?v_30 ?v_17))))) (and (and (not (= ?v_30 ?v_11)) (and (and (not (= ?v_11 ?v_34)) (not (= ?v_11 ?v_35))) (and (not (= ?v_30 ?v_18)) (not (= ?v_30 ?v_19))))) (and (and (not (= ?v_41 ?v_5)) (and (and (not (= ?v_5 ?v_50)) (not (= ?v_5 ?v_51))) (and (not (= ?v_41 ?v_12)) (not (= ?v_41 ?v_13))))) (and (and (not (= ?v_41 ?v_44)) (and (and (not (= ?v_44 ?v_50)) (not (= ?v_44 ?v_51))) (and (not (= ?v_41 ?v_52)) (not (= ?v_41 ?v_53))))) (and (and (not (= ?v_41 ?v_22)) (and (and (not (= ?v_22 ?v_50)) (not (= ?v_22 ?v_51))) (and (not (= ?v_41 ?v_23)) (not (= ?v_41 ?v_24))))) (and (and (not (= ?v_33 ?v_1)) (and (and (not (= ?v_1 ?v_46)) (not (= ?v_1 ?v_47))) (and (not (= ?v_33 ?v_16)) (not (= ?v_33 ?v_17))))) (and (and (not (= ?v_33 ?v_11)) (and (and (not (= ?v_11 ?v_46)) (not (= ?v_11 ?v_47))) (and (not (= ?v_33 ?v_18)) (not (= ?v_33 ?v_19))))) (and (and (not (= ?v_44 ?v_22)) (and (and (not (= ?v_22 ?v_52)) (not (= ?v_22 ?v_53))) (and (not (= ?v_44 ?v_23)) (not (= ?v_44 ?v_24))))) (and (and (not (= ?v_41 ?v_1)) (and (and (not (= ?v_1 ?v_50)) (not (= ?v_1 ?v_51))) (and (not (= ?v_41 ?v_16)) (not (= ?v_41 ?v_17))))) (and (and (not (= ?v_41 ?v_11)) (and (and (not (= ?v_11 ?v_50)) (not (= ?v_11 ?v_51))) (and (not (= ?v_41 ?v_18)) (not (= ?v_41 ?v_19))))) (and (valid ?v_25 ?v_61) (and (and (not (= ?v_44 ?v_1)) (and (and (not (= ?v_1 ?v_52)) (not (= ?v_1 ?v_53))) (and (not (= ?v_44 ?v_16)) (not (= ?v_44 ?v_17))))) (and (and (not (= ?v_44 ?v_11)) (and (and (not (= ?v_11 ?v_52)) (not (= ?v_11 ?v_53))) (and (not (= ?v_44 ?v_18)) (not (= ?v_44 ?v_19))))) (and (and (not (= ?v_56 ?v_30)) (and (and (not (= ?v_30 ?v_57)) (not (= ?v_30 ?v_58))) (and (not (= ?v_56 ?v_34)) (not (= ?v_56 ?v_35))))) (and (and (not (= ?v_56 ?v_28)) (and (and (not (= ?v_28 ?v_57)) (not (= ?v_28 ?v_58))) (and (not (= ?v_56 ?v_59)) (not (= ?v_56 ?v_60))))) (and (and (not (= ?v_56 ?v_33)) (and (and (not (= ?v_33 ?v_57)) (not (= ?v_33 ?v_58))) (and (not (= ?v_56 ?v_46)) (not (= ?v_56 ?v_47))))) (and (and (not (= ?v_56 ?v_38)) (and (and (not (= ?v_38 ?v_57)) (not (= ?v_38 ?v_58))) (and (not (= ?v_56 ?v_48)) (not (= ?v_56 ?v_49))))) (and (and (not (= ?v_63 ?v_56)) (and (and (not (= ?v_56 ?v_64)) (not (= ?v_56 ?v_65))) (and (not (= ?v_63 ?v_57)) (not (= ?v_63 ?v_58))))) (and (and (not (= ?v_56 ?v_41)) (and (and (not (= ?v_41 ?v_57)) (not (= ?v_41 ?v_58))) (and (not (= ?v_56 ?v_50)) (not (= ?v_56 ?v_51))))) (and (and (not (= ?v_63 ?v_30)) (and (and (not (= ?v_30 ?v_64)) (not (= ?v_30 ?v_65))) (and (not (= ?v_63 ?v_34)) (not (= ?v_63 ?v_35))))) (and (and (not (= ?v_56 ?v_5)) (and (and (not (= ?v_5 ?v_57)) (not (= ?v_5 ?v_58))) (and (not (= ?v_56 ?v_12)) (not (= ?v_56 ?v_13))))) (and (and (not (= ?v_63 ?v_28)) (and (and (not (= ?v_28 ?v_64)) (not (= ?v_28 ?v_65))) (and (not (= ?v_63 ?v_59)) (not (= ?v_63 ?v_60))))) (and (and (not (= ?v_56 ?v_44)) (and (and (not (= ?v_44 ?v_57)) (not (= ?v_44 ?v_58))) (and (not (= ?v_56 ?v_52)) (not (= ?v_56 ?v_53))))) (and (and (not (= ?v_63 ?v_33)) (and (and (not (= ?v_33 ?v_64)) (not (= ?v_33 ?v_65))) (and (not (= ?v_63 ?v_46)) (not (= ?v_63 ?v_47))))) (and (and (not (= ?v_56 ?v_22)) (and (and (not (= ?v_22 ?v_57)) (not (= ?v_22 ?v_58))) (and (not (= ?v_56 ?v_23)) (not (= ?v_56 ?v_24))))) (and (and (not (= ?v_63 ?v_38)) (and (and (not (= ?v_38 ?v_64)) (not (= ?v_38 ?v_65))) (and (not (= ?v_63 ?v_48)) (not (= ?v_63 ?v_49))))) (and (and (not (= ?v_63 ?v_41)) (and (and (not (= ?v_41 ?v_64)) (not (= ?v_41 ?v_65))) (and (not (= ?v_63 ?v_50)) (not (= ?v_63 ?v_51))))) (and (and (not (= ?v_63 ?v_5)) (and (and (not (= ?v_5 ?v_64)) (not (= ?v_5 ?v_65))) (and (not (= ?v_63 ?v_12)) (not (= ?v_63 ?v_13))))) (and (and (not (= ?v_63 ?v_44)) (and (and (not (= ?v_44 ?v_64)) (not (= ?v_44 ?v_65))) (and (not (= ?v_63 ?v_52)) (not (= ?v_63 ?v_53))))) (and (and (not (= ?v_63 ?v_22)) (and (and (not (= ?v_22 ?v_64)) (not (= ?v_22 ?v_65))) (and (not (= ?v_63 ?v_23)) (not (= ?v_63 ?v_24))))) (and (and (not (= ?v_28 ?v_33)) (and (and (not (= ?v_33 ?v_59)) (not (= ?v_33 ?v_60))) (and (not (= ?v_28 ?v_46)) (not (= ?v_28 ?v_47))))) (and (and (not (= ?v_28 ?v_38)) (and (and (not (= ?v_38 ?v_59)) (not (= ?v_38 ?v_60))) (and (not (= ?v_28 ?v_48)) (not (= ?v_28 ?v_49))))) (and (and (not (= ?v_28 ?v_41)) (and (and (not (= ?v_41 ?v_59)) (not (= ?v_41 ?v_60))) (and (not (= ?v_28 ?v_50)) (not (= ?v_28 ?v_51))))) (and (and (not (= ?v_28 ?v_5)) (and (and (not (= ?v_5 ?v_59)) (not (= ?v_5 ?v_60))) (and (not (= ?v_28 ?v_12)) (not (= ?v_28 ?v_13))))) (and (and (not (= ?v_28 ?v_44)) (and (and (not (= ?v_44 ?v_59)) (not (= ?v_44 ?v_60))) (and (not (= ?v_28 ?v_52)) (not (= ?v_28 ?v_53))))) (and (and (not (= ?v_28 ?v_22)) (and (and (not (= ?v_22 ?v_59)) (not (= ?v_22 ?v_60))) (and (not (= ?v_28 ?v_23)) (not (= ?v_28 ?v_24))))) (and (and (not (= ?v_56 ?v_1)) (and (and (not (= ?v_1 ?v_57)) (not (= ?v_1 ?v_58))) (and (not (= ?v_56 ?v_16)) (not (= ?v_56 ?v_17))))) (and (and (not (= ?v_56 ?v_11)) (and (and (not (= ?v_11 ?v_57)) (not (= ?v_11 ?v_58))) (and (not (= ?v_56 ?v_18)) (not (= ?v_56 ?v_19))))) (and (and (not (= ?v_63 ?v_1)) (and (and (not (= ?v_1 ?v_64)) (not (= ?v_1 ?v_65))) (and (not (= ?v_63 ?v_16)) (not (= ?v_63 ?v_17))))) (and (and (not (= ?v_63 ?v_11)) (and (and (not (= ?v_11 ?v_64)) (not (= ?v_11 ?v_65))) (and (not (= ?v_63 ?v_18)) (not (= ?v_63 ?v_19))))) (and (and (not (= ?v_38 ?v_41)) (and (and (not (= ?v_41 ?v_48)) (not (= ?v_41 ?v_49))) (and (not (= ?v_38 ?v_50)) (not (= ?v_38 ?v_51))))) (and (and (not (= ?v_38 ?v_5)) (and (and (not (= ?v_5 ?v_48)) (not (= ?v_5 ?v_49))) (and (not (= ?v_38 ?v_12)) (not (= ?v_38 ?v_13))))) (and (and (not (= ?v_38 ?v_44)) (and (and (not (= ?v_44 ?v_48)) (not (= ?v_44 ?v_49))) (and (not (= ?v_38 ?v_52)) (not (= ?v_38 ?v_53))))) (and (and (not (= ?v_38 ?v_22)) (and (and (not (= ?v_22 ?v_48)) (not (= ?v_22 ?v_49))) (and (not (= ?v_38 ?v_23)) (not (= ?v_38 ?v_24))))) (and (and (not (= ?v_28 ?v_1)) (and (and (not (= ?v_1 ?v_59)) (not (= ?v_1 ?v_60))) (and (not (= ?v_28 ?v_16)) (not (= ?v_28 ?v_17))))) (and (and (not (= ?v_28 ?v_11)) (and (and (not (= ?v_11 ?v_59)) (not (= ?v_11 ?v_60))) (and (not (= ?v_28 ?v_18)) (not (= ?v_28 ?v_19))))) (and (and (not (= ?v_5 ?v_44)) (and (and (not (= ?v_44 ?v_12)) (not (= ?v_44 ?v_13))) (and (not (= ?v_5 ?v_52)) (not (= ?v_5 ?v_53))))) (and (and (not (= ?v_5 ?v_22)) (and (and (not (= ?v_22 ?v_12)) (not (= ?v_22 ?v_13))) (and (not (= ?v_5 ?v_23)) (not (= ?v_5 ?v_24))))) (and (and (not (= ?v_38 ?v_1)) (and (and (not (= ?v_1 ?v_48)) (not (= ?v_1 ?v_49))) (and (not (= ?v_38 ?v_16)) (not (= ?v_38 ?v_17))))) (and (and (not (= ?v_38 ?v_11)) (and (and (not (= ?v_11 ?v_48)) (not (= ?v_11 ?v_49))) (and (not (= ?v_38 ?v_18)) (not (= ?v_38 ?v_19))))) (and (separation1 ?v_6 ?v_9) (and (valid_acc ?v_9) (and (valid_acc ?v_6) (and (valid_acc_range ?v_9 5) (valid_acc_range ?v_6 5))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (=> ?v_66 (forall ((?anonymous_2_v1_global0 c_unique)) (forall ((?anonymous_2_v2_global0 c_unique)) (forall ((?intM_global0 c_unique)) (let ((?v_67 (type_memory c_int type_global)) (?v_69 (type_pset type_global))) (let ((?v_68 (c_sort ?v_69 (pset_singleton ?v_14)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global) (c_sort ?v_67 ?anonymous_2_v1_global0) ?v_68) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global) (c_sort ?v_67 ?anonymous_2_v2_global0) ?v_68)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global) (c_sort ?v_67 ?intM_global0) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_14)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_14)))) 0 4)))))) (=> (valid ?v_25 ?v_8) (forall ((?anonymous_2_v1_global1 c_unique)) (forall ((?anonymous_2_v2_global1 c_unique)) (forall ((?intM_global1 c_unique)) (let ((?v_70 (c_sort ?v_69 (pset_singleton ?v_8)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global0) (c_sort ?v_67 ?anonymous_2_v1_global1) ?v_70) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global0) (c_sort ?v_67 ?anonymous_2_v2_global1) ?v_70)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global0) (c_sort ?v_67 ?intM_global1) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_8)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_8)))) 0 4)))))) (=> (valid ?v_25 ?v_20) (forall ((?anonymous_2_v1_global2 c_unique)) (forall ((?anonymous_2_v2_global2 c_unique)) (forall ((?intM_global2 c_unique)) (let ((?v_71 (c_sort ?v_69 (pset_singleton ?v_20)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global1) (c_sort ?v_67 ?anonymous_2_v1_global2) ?v_71) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global1) (c_sort ?v_67 ?anonymous_2_v2_global2) ?v_71)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global1) (c_sort ?v_67 ?intM_global2) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_20)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_20)))) 0 4)))))) (=> (valid ?v_25 ?v_43) (forall ((?anonymous_2_v1_global3 c_unique)) (forall ((?anonymous_2_v2_global3 c_unique)) (forall ((?intM_global3 c_unique)) (let ((?v_72 (c_sort ?v_69 (pset_singleton ?v_43)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global2) (c_sort ?v_67 ?anonymous_2_v1_global3) ?v_72) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global2) (c_sort ?v_67 ?anonymous_2_v2_global3) ?v_72)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global2) (c_sort ?v_67 ?intM_global3) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_43)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_43)))) 0 4)))))) (=> (valid ?v_25 ?v_3) (forall ((?anonymous_2_v1_global4 c_unique)) (forall ((?anonymous_2_v2_global4 c_unique)) (forall ((?intM_global4 c_unique)) (let ((?v_73 (c_sort ?v_69 (pset_singleton ?v_3)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global3) (c_sort ?v_67 ?anonymous_2_v1_global4) ?v_73) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global3) (c_sort ?v_67 ?anonymous_2_v2_global4) ?v_73)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global3) (c_sort ?v_67 ?intM_global4) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_3)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_3)))) 0 4)))))) (=> (valid ?v_25 ?v_40) (forall ((?anonymous_2_v1_global5 c_unique)) (forall ((?anonymous_2_v2_global5 c_unique)) (forall ((?intM_global5 c_unique)) (let ((?v_74 (c_sort ?v_69 (pset_singleton ?v_40)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global4) (c_sort ?v_67 ?anonymous_2_v1_global5) ?v_74) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global4) (c_sort ?v_67 ?anonymous_2_v2_global5) ?v_74)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global4) (c_sort ?v_67 ?intM_global5) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_40)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_40)))) 0 4)))))) (=> (valid ?v_25 ?v_37) (forall ((?anonymous_2_v1_global6 c_unique)) (forall ((?anonymous_2_v2_global6 c_unique)) (forall ((?intM_global6 c_unique)) (let ((?v_75 (c_sort ?v_69 (pset_singleton ?v_37)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global5) (c_sort ?v_67 ?anonymous_2_v1_global6) ?v_75) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global5) (c_sort ?v_67 ?anonymous_2_v2_global6) ?v_75)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global5) (c_sort ?v_67 ?intM_global6) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_37)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_37)))) 0 4)))))) (=> (valid ?v_25 ?v_32) (forall ((?anonymous_2_v1_global7 c_unique)) (forall ((?anonymous_2_v2_global7 c_unique)) (forall ((?intM_global7 c_unique)) (let ((?v_76 (c_sort ?v_69 (pset_singleton ?v_32)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global6) (c_sort ?v_67 ?anonymous_2_v1_global7) ?v_76) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global6) (c_sort ?v_67 ?anonymous_2_v2_global7) ?v_76)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global6) (c_sort ?v_67 ?intM_global7) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_32)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_32)))) 0 4)))))) (=> (valid ?v_25 ?v_27) (forall ((?anonymous_2_v1_global8 c_unique)) (forall ((?anonymous_2_v2_global8 c_unique)) (forall ((?intM_global8 c_unique)) (let ((?v_77 (c_sort ?v_69 (pset_singleton ?v_27))) (?v_78 (offset ?v_26))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global7) (c_sort ?v_67 ?anonymous_2_v1_global8) ?v_77) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global7) (c_sort ?v_67 ?anonymous_2_v2_global8) ?v_77)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global7) (c_sort ?v_67 ?intM_global8) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_27)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_27)))) 0 4)))))) (and (<= 0 ?v_78) (< ?v_78 (block_length ?v_25 ?v_26)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2-232-(check-sat)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-84-(declare-fun type_pointer (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:85:(declare-fun type_addr (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-86-(declare-fun type_alloc_table () c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-87-(declare-fun block_length (c_ssorted c_ssorted) Int)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:88:(declare-fun base_addr (c_ssorted) c_unique)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-89-(declare-fun offset (c_ssorted) Int)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-108-(assert (forall ((?t_12_122_70 c_type)) (forall ((?p_121_71 c_unique)) (forall ((?i_120_72 Int)) (forall ((?j_119_73 Int)) (let ((?v_0 (type_pointer ?t_12_122_70))) (let ((?v_1 (c_sort ?v_0 ?p_121_71))) (= (shift (c_sort ?v_0 (shift ?v_1 ?i_120_72)) ?j_119_73) (shift ?v_1 (+ ?i_120_72 ?j_119_73))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:109:(assert (forall ((?t_13_125_74 c_type)) (forall ((?p_124_75 c_unique)) (forall ((?i_123_76 Int)) (let ((?v_0 (type_pointer ?t_13_125_74))) (let ((?v_1 (c_sort ?v_0 ?p_124_75))) (= (base_addr (c_sort ?v_0 (shift ?v_1 ?i_123_76))) (base_addr ?v_1))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-110-(assert (forall ((?t_14_129_77 c_type)) (forall ((?a_128_78 c_unique)) (forall ((?p_127_79 c_unique)) (forall ((?i_126_80 Int)) (let ((?v_1 (c_sort type_alloc_table ?a_128_78)) (?v_0 (type_pointer ?t_14_129_77))) (let ((?v_2 (c_sort ?v_0 ?p_127_79))) (= (block_length ?v_1 (c_sort ?v_0 (shift ?v_2 ?i_126_80))) (block_length ?v_1 ?v_2)))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-152-(assert (forall ((?t_42_259_176 c_type)) (forall ((?t_41_258_177 c_type)) (forall ((?l_257_178 c_unique)) (forall ((?m_256_179 c_unique)) (forall ((?p_255_180 c_unique)) (let ((?v_0 (type_pointer ?t_42_259_176))) (=> (not_in_pset (c_sort ?v_0 ?p_255_180) (c_sort (type_pset ?t_42_259_176) (pset_star (c_sort (type_pset ?t_41_258_177) ?l_257_178) (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179)))) (forall ((?p1_254_181 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_41_258_177) ?p1_254_181))) (=> (= ?p_255_180 (acc (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_41_258_177) ?l_257_178)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:153:(assert (forall ((?t_43_263_182 c_type)) (forall ((?p_262_183 c_unique)) (forall ((?l_261_184 c_unique)) (let ((?v_0 (type_pset ?t_43_263_182))) (=> (forall ((?p1_260_185 c_unique)) (let ((?v_1 (type_pointer ?t_43_263_182))) (let ((?v_2 (c_sort ?v_1 ?p1_260_185))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_261_184))) (not (= (base_addr (c_sort ?v_1 ?p_262_183)) (base_addr ?v_2))))))) (not_in_pset (c_sort (type_pointer ?t_43_263_182) ?p_262_183) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_261_184))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:154:(assert (forall ((?t_44_267_186 c_type)) (forall ((?p_266_187 c_unique)) (forall ((?l_265_188 c_unique)) (let ((?v_0 (type_pset ?t_44_267_186))) (=> (not_in_pset (c_sort (type_pointer ?t_44_267_186) ?p_266_187) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_265_188)))) (forall ((?p1_264_189 c_unique)) (let ((?v_1 (type_pointer ?t_44_267_186))) (let ((?v_2 (c_sort ?v_1 ?p1_264_189))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_265_188))) (not (= (base_addr (c_sort ?v_1 ?p_266_187)) (base_addr ?v_2)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-155-(assert (forall ((?t_45_274_190 c_type)) (forall ((?p_273_191 c_unique)) (forall ((?l_272_192 c_unique)) (forall ((?a_271_193 Int)) (forall ((?b_270_194 Int)) (let ((?v_0 (type_pset ?t_45_274_190))) (=> (forall ((?p1_269_195 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) (c_sort ?v_0 ?l_272_192)) (forall ((?i_268_196 Int)) (=> (and (<= ?a_271_193 ?i_268_196) (<= ?i_268_196 ?b_270_194)) (not (= ?p_273_191 (shift (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) ?i_268_196))))))) (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p_273_191) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_272_192) ?a_271_193 ?b_270_194)))))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-176-(declare-fun separation1 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:177:(assert (forall ((?t_78_404_321 c_type)) (forall ((?t_77_403_322 c_type)) (forall ((?m1_402_323 c_unique)) (forall ((?m2_401_324 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_77_403_322) ?t_78_404_321))) (= (separation1 (c_sort ?v_0 ?m1_402_323) (c_sort ?v_0 ?m2_401_324)) (forall ((?p_400_325 c_unique)) (forall ((?a_399_326 c_unique)) (let ((?v_1 (type_pointer ?t_77_403_322)) (?v_2 (c_sort (type_pointer ?t_78_404_321) ?p_400_325))) (=> (valid (c_sort type_alloc_table ?a_399_326) ?v_2) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_402_323) ?v_2))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_401_324) ?v_2))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-178-(declare-fun separation1_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:179:(assert (forall ((?t_80_412_327 c_type)) (forall ((?t_79_411_328 c_type)) (forall ((?m1_410_329 c_unique)) (forall ((?m2_409_330 c_unique)) (forall ((?size_408_331 Int)) (let ((?v_0 (type_memory (type_pointer ?t_79_411_328) ?t_80_412_327))) (= (separation1_range1 (c_sort ?v_0 ?m1_410_329) (c_sort ?v_0 ?m2_409_330) ?size_408_331) (forall ((?p_407_332 c_unique)) (forall ((?a_406_333 c_unique)) (=> (valid (c_sort type_alloc_table ?a_406_333) (c_sort (type_pointer ?t_80_412_327) ?p_407_332)) (forall ((?i_405_334 Int)) (let ((?v_1 (type_pointer ?t_79_411_328)) (?v_2 (type_pointer ?t_80_412_327))) (let ((?v_3 (c_sort ?v_2 ?p_407_332))) (=> (and (<= 0 ?i_405_334) (< ?i_405_334 ?size_408_331)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_410_329) (c_sort ?v_2 (shift ?v_3 ?i_405_334))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_409_330) ?v_3))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-180-(declare-fun separation1_range (c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:181:(assert (forall ((?t_82_420_335 c_type)) (forall ((?t_81_419_336 c_type)) (forall ((?m_418_337 c_unique)) (forall ((?size_417_338 Int)) (= (separation1_range (c_sort (type_memory (type_pointer ?t_81_419_336) ?t_82_420_335) ?m_418_337) ?size_417_338) (forall ((?p_416_339 c_unique)) (forall ((?a_415_340 c_unique)) (=> (valid (c_sort type_alloc_table ?a_415_340) (c_sort (type_pointer ?t_82_420_335) ?p_416_339)) (forall ((?i1_414_341 Int)) (forall ((?i2_413_342 Int)) (let ((?v_0 (type_pointer ?t_81_419_336))) (let ((?v_2 (c_sort (type_memory ?v_0 ?t_82_420_335) ?m_418_337)) (?v_1 (type_pointer ?t_82_420_335))) (let ((?v_3 (c_sort ?v_1 ?p_416_339))) (=> (and (<= 0 ?i1_414_341) (< ?i1_414_341 ?size_417_338)) (=> (and (<= 0 ?i2_413_342) (< ?i2_413_342 ?size_417_338)) (=> (not (= ?i1_414_341 ?i2_413_342)) (not (= (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i1_414_341))))) (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i2_413_342))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-182-(declare-fun separation2 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:183:(assert (forall ((?t_84_426_343 c_type)) (forall ((?t_83_425_344 c_type)) (forall ((?m1_424_345 c_unique)) (forall ((?m2_423_346 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_83_425_344) ?t_84_426_343))) (= (separation2 (c_sort ?v_0 ?m1_424_345) (c_sort ?v_0 ?m2_423_346)) (forall ((?p1_422_347 c_unique)) (forall ((?p2_421_348 c_unique)) (let ((?v_1 (type_pointer ?t_83_425_344)) (?v_2 (type_pointer ?t_84_426_343))) (=> (not (= ?p1_422_347 ?p2_421_348)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_424_345) (c_sort ?v_2 ?p1_422_347)))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_423_346) (c_sort ?v_2 ?p2_421_348)))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-184-(declare-fun separation2_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2:185:(assert (forall ((?t_86_435_349 c_type)) (forall ((?t_85_434_350 c_type)) (forall ((?m1_433_351 c_unique)) (forall ((?m2_432_352 c_unique)) (forall ((?size_431_353 Int)) (let ((?v_0 (type_memory (type_pointer ?t_85_434_350) ?t_86_435_349))) (= (separation2_range1 (c_sort ?v_0 ?m1_433_351) (c_sort ?v_0 ?m2_432_352) ?size_431_353) (forall ((?p_430_354 c_unique)) (forall ((?q_429_355 c_unique)) (forall ((?a_428_356 c_unique)) (forall ((?i_427_357 Int)) (let ((?v_1 (type_pointer ?t_85_434_350)) (?v_2 (type_pointer ?t_86_435_349))) (=> (and (<= 0 ?i_427_357) (< ?i_427_357 ?size_431_353)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_433_351) (c_sort ?v_2 (shift (c_sort ?v_2 ?p_430_354) ?i_427_357))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_432_352) (c_sort ?v_2 ?q_429_355))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib384a03.smt2-186-(declare-fun on_heap (c_ssorted c_ssorted) Bool)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-84-(declare-fun type_pointer (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:85:(declare-fun type_addr (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-86-(declare-fun type_alloc_table () c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-87-(declare-fun block_length (c_ssorted c_ssorted) Int)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:88:(declare-fun base_addr (c_ssorted) c_unique)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-89-(declare-fun offset (c_ssorted) Int)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-108-(assert (forall ((?t_12_122_70 c_type)) (forall ((?p_121_71 c_unique)) (forall ((?i_120_72 Int)) (forall ((?j_119_73 Int)) (let ((?v_0 (type_pointer ?t_12_122_70))) (let ((?v_1 (c_sort ?v_0 ?p_121_71))) (= (shift (c_sort ?v_0 (shift ?v_1 ?i_120_72)) ?j_119_73) (shift ?v_1 (+ ?i_120_72 ?j_119_73))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:109:(assert (forall ((?t_13_125_74 c_type)) (forall ((?p_124_75 c_unique)) (forall ((?i_123_76 Int)) (let ((?v_0 (type_pointer ?t_13_125_74))) (let ((?v_1 (c_sort ?v_0 ?p_124_75))) (= (base_addr (c_sort ?v_0 (shift ?v_1 ?i_123_76))) (base_addr ?v_1))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-110-(assert (forall ((?t_14_129_77 c_type)) (forall ((?a_128_78 c_unique)) (forall ((?p_127_79 c_unique)) (forall ((?i_126_80 Int)) (let ((?v_1 (c_sort type_alloc_table ?a_128_78)) (?v_0 (type_pointer ?t_14_129_77))) (let ((?v_2 (c_sort ?v_0 ?p_127_79))) (= (block_length ?v_1 (c_sort ?v_0 (shift ?v_2 ?i_126_80))) (block_length ?v_1 ?v_2)))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-152-(assert (forall ((?t_42_259_176 c_type)) (forall ((?t_41_258_177 c_type)) (forall ((?l_257_178 c_unique)) (forall ((?m_256_179 c_unique)) (forall ((?p_255_180 c_unique)) (let ((?v_0 (type_pointer ?t_42_259_176))) (=> (not_in_pset (c_sort ?v_0 ?p_255_180) (c_sort (type_pset ?t_42_259_176) (pset_star (c_sort (type_pset ?t_41_258_177) ?l_257_178) (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179)))) (forall ((?p1_254_181 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_41_258_177) ?p1_254_181))) (=> (= ?p_255_180 (acc (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_41_258_177) ?l_257_178)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:153:(assert (forall ((?t_43_263_182 c_type)) (forall ((?p_262_183 c_unique)) (forall ((?l_261_184 c_unique)) (let ((?v_0 (type_pset ?t_43_263_182))) (=> (forall ((?p1_260_185 c_unique)) (let ((?v_1 (type_pointer ?t_43_263_182))) (let ((?v_2 (c_sort ?v_1 ?p1_260_185))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_261_184))) (not (= (base_addr (c_sort ?v_1 ?p_262_183)) (base_addr ?v_2))))))) (not_in_pset (c_sort (type_pointer ?t_43_263_182) ?p_262_183) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_261_184))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:154:(assert (forall ((?t_44_267_186 c_type)) (forall ((?p_266_187 c_unique)) (forall ((?l_265_188 c_unique)) (let ((?v_0 (type_pset ?t_44_267_186))) (=> (not_in_pset (c_sort (type_pointer ?t_44_267_186) ?p_266_187) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_265_188)))) (forall ((?p1_264_189 c_unique)) (let ((?v_1 (type_pointer ?t_44_267_186))) (let ((?v_2 (c_sort ?v_1 ?p1_264_189))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_265_188))) (not (= (base_addr (c_sort ?v_1 ?p_266_187)) (base_addr ?v_2)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-155-(assert (forall ((?t_45_274_190 c_type)) (forall ((?p_273_191 c_unique)) (forall ((?l_272_192 c_unique)) (forall ((?a_271_193 Int)) (forall ((?b_270_194 Int)) (let ((?v_0 (type_pset ?t_45_274_190))) (=> (forall ((?p1_269_195 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) (c_sort ?v_0 ?l_272_192)) (forall ((?i_268_196 Int)) (=> (and (<= ?a_271_193 ?i_268_196) (<= ?i_268_196 ?b_270_194)) (not (= ?p_273_191 (shift (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) ?i_268_196))))))) (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p_273_191) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_272_192) ?a_271_193 ?b_270_194)))))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-176-(declare-fun separation1 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:177:(assert (forall ((?t_78_404_321 c_type)) (forall ((?t_77_403_322 c_type)) (forall ((?m1_402_323 c_unique)) (forall ((?m2_401_324 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_77_403_322) ?t_78_404_321))) (= (separation1 (c_sort ?v_0 ?m1_402_323) (c_sort ?v_0 ?m2_401_324)) (forall ((?p_400_325 c_unique)) (forall ((?a_399_326 c_unique)) (let ((?v_1 (type_pointer ?t_77_403_322)) (?v_2 (c_sort (type_pointer ?t_78_404_321) ?p_400_325))) (=> (valid (c_sort type_alloc_table ?a_399_326) ?v_2) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_402_323) ?v_2))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_401_324) ?v_2))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-178-(declare-fun separation1_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:179:(assert (forall ((?t_80_412_327 c_type)) (forall ((?t_79_411_328 c_type)) (forall ((?m1_410_329 c_unique)) (forall ((?m2_409_330 c_unique)) (forall ((?size_408_331 Int)) (let ((?v_0 (type_memory (type_pointer ?t_79_411_328) ?t_80_412_327))) (= (separation1_range1 (c_sort ?v_0 ?m1_410_329) (c_sort ?v_0 ?m2_409_330) ?size_408_331) (forall ((?p_407_332 c_unique)) (forall ((?a_406_333 c_unique)) (=> (valid (c_sort type_alloc_table ?a_406_333) (c_sort (type_pointer ?t_80_412_327) ?p_407_332)) (forall ((?i_405_334 Int)) (let ((?v_1 (type_pointer ?t_79_411_328)) (?v_2 (type_pointer ?t_80_412_327))) (let ((?v_3 (c_sort ?v_2 ?p_407_332))) (=> (and (<= 0 ?i_405_334) (< ?i_405_334 ?size_408_331)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_410_329) (c_sort ?v_2 (shift ?v_3 ?i_405_334))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_409_330) ?v_3))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-180-(declare-fun separation1_range (c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:181:(assert (forall ((?t_82_420_335 c_type)) (forall ((?t_81_419_336 c_type)) (forall ((?m_418_337 c_unique)) (forall ((?size_417_338 Int)) (= (separation1_range (c_sort (type_memory (type_pointer ?t_81_419_336) ?t_82_420_335) ?m_418_337) ?size_417_338) (forall ((?p_416_339 c_unique)) (forall ((?a_415_340 c_unique)) (=> (valid (c_sort type_alloc_table ?a_415_340) (c_sort (type_pointer ?t_82_420_335) ?p_416_339)) (forall ((?i1_414_341 Int)) (forall ((?i2_413_342 Int)) (let ((?v_0 (type_pointer ?t_81_419_336))) (let ((?v_2 (c_sort (type_memory ?v_0 ?t_82_420_335) ?m_418_337)) (?v_1 (type_pointer ?t_82_420_335))) (let ((?v_3 (c_sort ?v_1 ?p_416_339))) (=> (and (<= 0 ?i1_414_341) (< ?i1_414_341 ?size_417_338)) (=> (and (<= 0 ?i2_413_342) (< ?i2_413_342 ?size_417_338)) (=> (not (= ?i1_414_341 ?i2_413_342)) (not (= (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i1_414_341))))) (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i2_413_342))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-182-(declare-fun separation2 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:183:(assert (forall ((?t_84_426_343 c_type)) (forall ((?t_83_425_344 c_type)) (forall ((?m1_424_345 c_unique)) (forall ((?m2_423_346 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_83_425_344) ?t_84_426_343))) (= (separation2 (c_sort ?v_0 ?m1_424_345) (c_sort ?v_0 ?m2_423_346)) (forall ((?p1_422_347 c_unique)) (forall ((?p2_421_348 c_unique)) (let ((?v_1 (type_pointer ?t_83_425_344)) (?v_2 (type_pointer ?t_84_426_343))) (=> (not (= ?p1_422_347 ?p2_421_348)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_424_345) (c_sort ?v_2 ?p1_422_347)))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_423_346) (c_sort ?v_2 ?p2_421_348)))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-184-(declare-fun separation2_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2:185:(assert (forall ((?t_86_435_349 c_type)) (forall ((?t_85_434_350 c_type)) (forall ((?m1_433_351 c_unique)) (forall ((?m2_432_352 c_unique)) (forall ((?size_431_353 Int)) (let ((?v_0 (type_memory (type_pointer ?t_85_434_350) ?t_86_435_349))) (= (separation2_range1 (c_sort ?v_0 ?m1_433_351) (c_sort ?v_0 ?m2_432_352) ?size_431_353) (forall ((?p_430_354 c_unique)) (forall ((?q_429_355 c_unique)) (forall ((?a_428_356 c_unique)) (forall ((?i_427_357 Int)) (let ((?v_1 (type_pointer ?t_85_434_350)) (?v_2 (type_pointer ?t_86_435_349))) (=> (and (<= 0 ?i_427_357) (< ?i_427_357 ?size_431_353)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_433_351) (c_sort ?v_2 (shift (c_sort ?v_2 ?p_430_354) ?i_427_357))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_432_352) (c_sort ?v_2 ?q_429_355))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlib46f14a.smt2-186-(declare-fun on_heap (c_ssorted c_ssorted) Bool)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-83-(declare-fun type_pointer (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:84:(declare-fun type_addr (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-85-(declare-fun type_alloc_table () c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-86-(declare-fun block_length (c_ssorted c_ssorted) Int)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:87:(declare-fun base_addr (c_ssorted) c_unique)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-88-(declare-fun offset (c_ssorted) Int)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-107-(assert (forall ((?t_12_122_70 c_type)) (forall ((?p_121_71 c_unique)) (forall ((?i_120_72 Int)) (forall ((?j_119_73 Int)) (let ((?v_0 (type_pointer ?t_12_122_70))) (let ((?v_1 (c_sort ?v_0 ?p_121_71))) (= (shift (c_sort ?v_0 (shift ?v_1 ?i_120_72)) ?j_119_73) (shift ?v_1 (+ ?i_120_72 ?j_119_73))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:108:(assert (forall ((?t_13_125_74 c_type)) (forall ((?p_124_75 c_unique)) (forall ((?i_123_76 Int)) (let ((?v_0 (type_pointer ?t_13_125_74))) (let ((?v_1 (c_sort ?v_0 ?p_124_75))) (= (base_addr (c_sort ?v_0 (shift ?v_1 ?i_123_76))) (base_addr ?v_1))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-109-(assert (forall ((?t_14_129_77 c_type)) (forall ((?a_128_78 c_unique)) (forall ((?p_127_79 c_unique)) (forall ((?i_126_80 Int)) (let ((?v_1 (c_sort type_alloc_table ?a_128_78)) (?v_0 (type_pointer ?t_14_129_77))) (let ((?v_2 (c_sort ?v_0 ?p_127_79))) (= (block_length ?v_1 (c_sort ?v_0 (shift ?v_2 ?i_126_80))) (block_length ?v_1 ?v_2)))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-151-(assert (forall ((?t_42_259_176 c_type)) (forall ((?t_41_258_177 c_type)) (forall ((?l_257_178 c_unique)) (forall ((?m_256_179 c_unique)) (forall ((?p_255_180 c_unique)) (let ((?v_0 (type_pointer ?t_42_259_176))) (=> (not_in_pset (c_sort ?v_0 ?p_255_180) (c_sort (type_pset ?t_42_259_176) (pset_star (c_sort (type_pset ?t_41_258_177) ?l_257_178) (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179)))) (forall ((?p1_254_181 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_41_258_177) ?p1_254_181))) (=> (= ?p_255_180 (acc (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_41_258_177) ?l_257_178)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:152:(assert (forall ((?t_43_263_182 c_type)) (forall ((?p_262_183 c_unique)) (forall ((?l_261_184 c_unique)) (let ((?v_0 (type_pset ?t_43_263_182))) (=> (forall ((?p1_260_185 c_unique)) (let ((?v_1 (type_pointer ?t_43_263_182))) (let ((?v_2 (c_sort ?v_1 ?p1_260_185))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_261_184))) (not (= (base_addr (c_sort ?v_1 ?p_262_183)) (base_addr ?v_2))))))) (not_in_pset (c_sort (type_pointer ?t_43_263_182) ?p_262_183) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_261_184))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:153:(assert (forall ((?t_44_267_186 c_type)) (forall ((?p_266_187 c_unique)) (forall ((?l_265_188 c_unique)) (let ((?v_0 (type_pset ?t_44_267_186))) (=> (not_in_pset (c_sort (type_pointer ?t_44_267_186) ?p_266_187) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_265_188)))) (forall ((?p1_264_189 c_unique)) (let ((?v_1 (type_pointer ?t_44_267_186))) (let ((?v_2 (c_sort ?v_1 ?p1_264_189))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_265_188))) (not (= (base_addr (c_sort ?v_1 ?p_266_187)) (base_addr ?v_2)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-154-(assert (forall ((?t_45_274_190 c_type)) (forall ((?p_273_191 c_unique)) (forall ((?l_272_192 c_unique)) (forall ((?a_271_193 Int)) (forall ((?b_270_194 Int)) (let ((?v_0 (type_pset ?t_45_274_190))) (=> (forall ((?p1_269_195 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) (c_sort ?v_0 ?l_272_192)) (forall ((?i_268_196 Int)) (=> (and (<= ?a_271_193 ?i_268_196) (<= ?i_268_196 ?b_270_194)) (not (= ?p_273_191 (shift (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) ?i_268_196))))))) (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p_273_191) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_272_192) ?a_271_193 ?b_270_194)))))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-175-(declare-fun separation1 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:176:(assert (forall ((?t_78_404_321 c_type)) (forall ((?t_77_403_322 c_type)) (forall ((?m1_402_323 c_unique)) (forall ((?m2_401_324 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_77_403_322) ?t_78_404_321))) (= (separation1 (c_sort ?v_0 ?m1_402_323) (c_sort ?v_0 ?m2_401_324)) (forall ((?p_400_325 c_unique)) (forall ((?a_399_326 c_unique)) (let ((?v_1 (type_pointer ?t_77_403_322)) (?v_2 (c_sort (type_pointer ?t_78_404_321) ?p_400_325))) (=> (valid (c_sort type_alloc_table ?a_399_326) ?v_2) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_402_323) ?v_2))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_401_324) ?v_2))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-177-(declare-fun separation1_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:178:(assert (forall ((?t_80_412_327 c_type)) (forall ((?t_79_411_328 c_type)) (forall ((?m1_410_329 c_unique)) (forall ((?m2_409_330 c_unique)) (forall ((?size_408_331 Int)) (let ((?v_0 (type_memory (type_pointer ?t_79_411_328) ?t_80_412_327))) (= (separation1_range1 (c_sort ?v_0 ?m1_410_329) (c_sort ?v_0 ?m2_409_330) ?size_408_331) (forall ((?p_407_332 c_unique)) (forall ((?a_406_333 c_unique)) (=> (valid (c_sort type_alloc_table ?a_406_333) (c_sort (type_pointer ?t_80_412_327) ?p_407_332)) (forall ((?i_405_334 Int)) (let ((?v_1 (type_pointer ?t_79_411_328)) (?v_2 (type_pointer ?t_80_412_327))) (let ((?v_3 (c_sort ?v_2 ?p_407_332))) (=> (and (<= 0 ?i_405_334) (< ?i_405_334 ?size_408_331)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_410_329) (c_sort ?v_2 (shift ?v_3 ?i_405_334))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_409_330) ?v_3))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-179-(declare-fun separation1_range (c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:180:(assert (forall ((?t_82_420_335 c_type)) (forall ((?t_81_419_336 c_type)) (forall ((?m_418_337 c_unique)) (forall ((?size_417_338 Int)) (= (separation1_range (c_sort (type_memory (type_pointer ?t_81_419_336) ?t_82_420_335) ?m_418_337) ?size_417_338) (forall ((?p_416_339 c_unique)) (forall ((?a_415_340 c_unique)) (=> (valid (c_sort type_alloc_table ?a_415_340) (c_sort (type_pointer ?t_82_420_335) ?p_416_339)) (forall ((?i1_414_341 Int)) (forall ((?i2_413_342 Int)) (let ((?v_0 (type_pointer ?t_81_419_336))) (let ((?v_2 (c_sort (type_memory ?v_0 ?t_82_420_335) ?m_418_337)) (?v_1 (type_pointer ?t_82_420_335))) (let ((?v_3 (c_sort ?v_1 ?p_416_339))) (=> (and (<= 0 ?i1_414_341) (< ?i1_414_341 ?size_417_338)) (=> (and (<= 0 ?i2_413_342) (< ?i2_413_342 ?size_417_338)) (=> (not (= ?i1_414_341 ?i2_413_342)) (not (= (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i1_414_341))))) (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i2_413_342))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-181-(declare-fun separation2 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:182:(assert (forall ((?t_84_426_343 c_type)) (forall ((?t_83_425_344 c_type)) (forall ((?m1_424_345 c_unique)) (forall ((?m2_423_346 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_83_425_344) ?t_84_426_343))) (= (separation2 (c_sort ?v_0 ?m1_424_345) (c_sort ?v_0 ?m2_423_346)) (forall ((?p1_422_347 c_unique)) (forall ((?p2_421_348 c_unique)) (let ((?v_1 (type_pointer ?t_83_425_344)) (?v_2 (type_pointer ?t_84_426_343))) (=> (not (= ?p1_422_347 ?p2_421_348)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_424_345) (c_sort ?v_2 ?p1_422_347)))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_423_346) (c_sort ?v_2 ?p2_421_348)))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-183-(declare-fun separation2_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:184:(assert (forall ((?t_86_435_349 c_type)) (forall ((?t_85_434_350 c_type)) (forall ((?m1_433_351 c_unique)) (forall ((?m2_432_352 c_unique)) (forall ((?size_431_353 Int)) (let ((?v_0 (type_memory (type_pointer ?t_85_434_350) ?t_86_435_349))) (= (separation2_range1 (c_sort ?v_0 ?m1_433_351) (c_sort ?v_0 ?m2_432_352) ?size_431_353) (forall ((?p_430_354 c_unique)) (forall ((?q_429_355 c_unique)) (forall ((?a_428_356 c_unique)) (forall ((?i_427_357 Int)) (let ((?v_1 (type_pointer ?t_85_434_350)) (?v_2 (type_pointer ?t_86_435_349))) (=> (and (<= 0 ?i_427_357) (< ?i_427_357 ?size_431_353)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_433_351) (c_sort ?v_2 (shift (c_sort ?v_2 ?p_430_354) ?i_427_357))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_432_352) (c_sort ?v_2 ?q_429_355))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-185-(declare-fun on_heap (c_ssorted c_ssorted) Bool)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-202-(declare-fun separation_anonymous_0_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:203:(assert (forall ((?x_global_489_396 c_unique)) (forall ((?anonymous_0PM_global_488_397 c_unique)) (forall ((?tab_487_398 c_unique)) (forall ((?v_486_399 c_unique)) (forall ((?alloc_485_400 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global)) (?v_2 (c_sort ?v_1 ?tab_487_398)) (?v_3 (c_sort ?v_1 ?v_486_399))) (= (separation_anonymous_0_int (c_sort ?v_0 ?x_global_489_396) (c_sort ?v_0 ?anonymous_0PM_global_488_397) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_485_400)) (and (not (= (base_addr ?v_2) (base_addr ?v_3))) (forall ((?index_3_484_401 Int)) (=> (and (<= 0 ?index_3_484_401) (< ?index_3_484_401 5)) (not (= (base_addr ?v_3) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_489_396) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_488_397) (c_sort ?v_1 (shift ?v_2 ?index_3_484_401)))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-204-(declare-fun separation_anonymous_0_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:205:(assert (forall ((?x_global_498_402 c_unique)) (forall ((?u_global_497_403 c_unique)) (forall ((?t_global_496_404 c_unique)) (forall ((?s1PM_global_495_405 c_unique)) (forall ((?anonymous_0PM_global_494_406 c_unique)) (forall ((?tab_493_407 c_unique)) (forall ((?s_492_408 c_unique)) (forall ((?alloc_491_409 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_497_403)) (?v_5 (c_sort ?v_0 ?t_global_496_404)) (?v_6 (c_sort ?v_0 ?s1PM_global_495_405)) (?v_2 (c_sort ?v_1 ?tab_493_407)) (?v_3 (c_sort ?v_1 ?s_492_408))) (let ((?v_4 (base_addr ?v_2)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_0_s1 (c_sort ?v_0 ?x_global_498_402) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_494_406) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_491_409)) (and (not (= ?v_4 (base_addr ?v_3))) (and (forall ((?index_6_490_410 Int)) (=> (and (<= 0 ?index_6_490_410) (< ?index_6_490_410 5)) (not (= (base_addr ?v_3) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_498_402) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_494_406) (c_sort ?v_1 (shift ?v_2 ?index_6_490_410))))))))))) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-206-(declare-fun separation_anonymous_1_anonymous_0 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:207:(assert (forall ((?x_global_507_411 c_unique)) (forall ((?p2_global_506_412 c_unique)) (forall ((?p1_global_505_413 c_unique)) (forall ((?anonymous_1PM_global_504_414 c_unique)) (forall ((?anonymous_0PM_global_503_415 c_unique)) (forall ((?u1_502_416 c_unique)) (forall ((?tab_501_417 c_unique)) (forall ((?alloc_500_418 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_506_412)) (?v_5 (c_sort ?v_0 ?p1_global_505_413)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_504_414)) (?v_2 (c_sort ?v_1 ?u1_502_416)) (?v_3 (c_sort ?v_1 ?tab_501_417))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_1_anonymous_0 (c_sort ?v_0 ?x_global_507_411) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_503_415) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_500_418)) (and (not (= (base_addr ?v_2) ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (forall ((?index_7_499_419 Int)) (=> (and (<= 0 ?index_7_499_419) (< ?index_7_499_419 5)) (not (= (base_addr ?v_2) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_507_411) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_503_415) (c_sort ?v_1 (shift ?v_3 ?index_7_499_419)))))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-208-(declare-fun separation_anonymous_1_anonymous_1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:209:(assert (forall ((?p2_global_513_420 c_unique)) (forall ((?p1_global_512_421 c_unique)) (forall ((?anonymous_1PM_global_511_422 c_unique)) (forall ((?u2_510_423 c_unique)) (forall ((?u1_509_424 c_unique)) (forall ((?alloc_508_425 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_513_420)) (?v_5 (c_sort ?v_0 ?p1_global_512_421)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_511_422)) (?v_2 (c_sort ?v_1 ?u2_510_423)) (?v_3 (c_sort ?v_1 ?u1_509_424))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_1_anonymous_1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_508_425)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-210-(declare-fun separation_anonymous_1_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:211:(assert (forall ((?p2_global_519_426 c_unique)) (forall ((?p1_global_518_427 c_unique)) (forall ((?anonymous_1PM_global_517_428 c_unique)) (forall ((?u1_516_429 c_unique)) (forall ((?v_515_430 c_unique)) (forall ((?alloc_514_431 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_519_426)) (?v_5 (c_sort ?v_0 ?p1_global_518_427)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_517_428)) (?v_2 (c_sort ?v_1 ?u1_516_429)) (?v_3 (c_sort ?v_1 ?v_515_430))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_1_int ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_514_431)) (and (not (= (base_addr ?v_2) ?v_4)) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-212-(declare-fun separation_anonymous_1_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:213:(assert (forall ((?u_global_528_432 c_unique)) (forall ((?t_global_527_433 c_unique)) (forall ((?s1PM_global_526_434 c_unique)) (forall ((?p2_global_525_435 c_unique)) (forall ((?p1_global_524_436 c_unique)) (forall ((?anonymous_1PM_global_523_437 c_unique)) (forall ((?u1_522_438 c_unique)) (forall ((?s_521_439 c_unique)) (forall ((?alloc_520_440 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?u_global_528_432)) (?v_10 (c_sort ?v_0 ?t_global_527_433)) (?v_11 (c_sort ?v_0 ?s1PM_global_526_434)) (?v_7 (c_sort ?v_0 ?p2_global_525_435)) (?v_5 (c_sort ?v_0 ?p1_global_524_436)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_523_437)) (?v_2 (c_sort ?v_1 ?u1_522_438)) (?v_3 (c_sort ?v_1 ?s_521_439))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_1_s1 ?v_12 ?v_10 ?v_11 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_520_440)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-214-(declare-fun separation_anonymous_2_anonymous_0 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:215:(assert (forall ((?x_global_537_441 c_unique)) (forall ((?anonymous_2_p2_global_536_442 c_unique)) (forall ((?anonymous_2_p1_global_535_443 c_unique)) (forall ((?anonymous_2PM_global_534_444 c_unique)) (forall ((?anonymous_0PM_global_533_445 c_unique)) (forall ((?u3_532_446 c_unique)) (forall ((?tab_531_447 c_unique)) (forall ((?alloc_530_448 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_536_442)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_535_443)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_534_444)) (?v_2 (c_sort ?v_1 ?u3_532_446)) (?v_3 (c_sort ?v_1 ?tab_531_447))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_2_anonymous_0 (c_sort ?v_0 ?x_global_537_441) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_533_445) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_530_448)) (and (not (= (base_addr ?v_2) ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (forall ((?index_15_529_449 Int)) (=> (and (<= 0 ?index_15_529_449) (< ?index_15_529_449 5)) (not (= (base_addr ?v_2) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_537_441) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_533_445) (c_sort ?v_1 (shift ?v_3 ?index_15_529_449)))))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-216-(declare-fun separation_anonymous_2_anonymous_1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:217:(assert (forall ((?p2_global_546_450 c_unique)) (forall ((?p1_global_545_451 c_unique)) (forall ((?anonymous_2_p2_global_544_452 c_unique)) (forall ((?anonymous_2_p1_global_543_453 c_unique)) (forall ((?anonymous_2PM_global_542_454 c_unique)) (forall ((?anonymous_1PM_global_541_455 c_unique)) (forall ((?u3_540_456 c_unique)) (forall ((?u1_539_457 c_unique)) (forall ((?alloc_538_458 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?p2_global_546_450)) (?v_10 (c_sort ?v_0 ?p1_global_545_451)) (?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_544_452)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_543_453)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_542_454)) (?v_11 (c_sort ?v_0 ?anonymous_1PM_global_541_455)) (?v_2 (c_sort ?v_1 ?u3_540_456)) (?v_3 (c_sort ?v_1 ?u1_539_457))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_2_anonymous_1 ?v_12 ?v_10 ?v_7 ?v_5 ?v_6 ?v_11 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_538_458)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-218-(declare-fun separation_anonymous_2_anonymous_2 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:219:(assert (forall ((?anonymous_2_p2_global_552_459 c_unique)) (forall ((?anonymous_2_p1_global_551_460 c_unique)) (forall ((?anonymous_2PM_global_550_461 c_unique)) (forall ((?u4_549_462 c_unique)) (forall ((?u3_548_463 c_unique)) (forall ((?alloc_547_464 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_552_459)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_551_460)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_550_461)) (?v_2 (c_sort ?v_1 ?u4_549_462)) (?v_3 (c_sort ?v_1 ?u3_548_463))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_2_anonymous_2 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_547_464)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-220-(declare-fun separation_anonymous_2_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:221:(assert (forall ((?anonymous_2_p2_global_558_465 c_unique)) (forall ((?anonymous_2_p1_global_557_466 c_unique)) (forall ((?anonymous_2PM_global_556_467 c_unique)) (forall ((?u3_555_468 c_unique)) (forall ((?v_554_469 c_unique)) (forall ((?alloc_553_470 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_558_465)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_557_466)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_556_467)) (?v_2 (c_sort ?v_1 ?u3_555_468)) (?v_3 (c_sort ?v_1 ?v_554_469))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_2_int ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_553_470)) (and (not (= (base_addr ?v_2) ?v_4)) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-222-(declare-fun separation_anonymous_2_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:223:(assert (forall ((?u_global_567_471 c_unique)) (forall ((?t_global_566_472 c_unique)) (forall ((?s1PM_global_565_473 c_unique)) (forall ((?anonymous_2_p2_global_564_474 c_unique)) (forall ((?anonymous_2_p1_global_563_475 c_unique)) (forall ((?anonymous_2PM_global_562_476 c_unique)) (forall ((?u3_561_477 c_unique)) (forall ((?s_560_478 c_unique)) (forall ((?alloc_559_479 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?u_global_567_471)) (?v_10 (c_sort ?v_0 ?t_global_566_472)) (?v_11 (c_sort ?v_0 ?s1PM_global_565_473)) (?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_564_474)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_563_475)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_562_476)) (?v_2 (c_sort ?v_1 ?u3_561_477)) (?v_3 (c_sort ?v_1 ?s_560_478))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_2_s1 ?v_12 ?v_10 ?v_11 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_559_479)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13)))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-224-(declare-fun separation_int_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:225:(assert (forall ((?u_global_573_480 c_unique)) (forall ((?t_global_572_481 c_unique)) (forall ((?s1PM_global_571_482 c_unique)) (forall ((?v_570_483 c_unique)) (forall ((?s_569_484 c_unique)) (forall ((?alloc_568_485 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_573_480)) (?v_5 (c_sort ?v_0 ?t_global_572_481)) (?v_6 (c_sort ?v_0 ?s1PM_global_571_482)) (?v_2 (c_sort ?v_1 ?v_570_483)) (?v_3 (c_sort ?v_1 ?s_569_484))) (let ((?v_4 (base_addr ?v_2)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_int_s1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_568_485)) (and (not (= ?v_4 (base_addr ?v_3))) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-226-(declare-fun separation_s1_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:227:(assert (forall ((?u_global_579_486 c_unique)) (forall ((?t_global_578_487 c_unique)) (forall ((?s1PM_global_577_488 c_unique)) (forall ((?ss_576_489 c_unique)) (forall ((?s_575_490 c_unique)) (forall ((?alloc_574_491 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_579_486)) (?v_5 (c_sort ?v_0 ?t_global_578_487)) (?v_6 (c_sort ?v_0 ?s1PM_global_577_488)) (?v_2 (c_sort ?v_1 ?ss_576_489)) (?v_3 (c_sort ?v_1 ?s_575_490))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_s1_s1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_574_491)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2:228:(assert (not (forall ((?alloc c_unique)) (forall ((?anonymous_2PM_global c_unique)) (forall ((?anonymous_2_p1_global c_unique)) (forall ((?anonymous_2_p2_global c_unique)) (forall ((?anonymous_2_v1_global c_unique)) (forall ((?anonymous_2_v2_global c_unique)) (forall ((?intM_global c_unique)) (forall ((?u3 c_unique)) (forall ((?u4 c_unique)) (forall ((?w1 c_unique)) (forall ((?w10 c_unique)) (forall ((?w2 c_unique)) (forall ((?w3 c_unique)) (forall ((?w4 c_unique)) (forall ((?w5 c_unique)) (forall ((?w6 c_unique)) (forall ((?w7 c_unique)) (forall ((?w8 c_unique)) (forall ((?w9 c_unique)) (let ((?v_0 (type_pointer type_global))) (let ((?v_2 (type_memory ?v_0 type_global)) (?v_3 (c_sort ?v_0 ?w3))) (let ((?v_5 (base_addr ?v_3)) (?v_8 (c_sort ?v_0 ?u4))) (let ((?v_1 (base_addr ?v_8)) (?v_6 (c_sort ?v_2 ?anonymous_2_p1_global)) (?v_7 (c_sort ?v_2 ?anonymous_2PM_global))) (let ((?v_4 (c_sort ?v_0 (acc ?v_7 ?v_3)))) (let ((?v_12 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_4)))) (?v_9 (c_sort ?v_2 ?anonymous_2_p2_global))) (let ((?v_13 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_4)))) (?v_10 (c_sort ?v_0 (acc ?v_7 ?v_8)))) (let ((?v_16 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_10)))) (?v_17 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_10)))) (?v_14 (c_sort ?v_0 ?u3))) (let ((?v_11 (base_addr ?v_14)) (?v_15 (c_sort ?v_0 (acc ?v_7 ?v_14)))) (let ((?v_18 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_15)))) (?v_19 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_15)))) (?v_20 (c_sort ?v_0 ?w1))) (let ((?v_22 (base_addr ?v_20)) (?v_21 (c_sort ?v_0 (acc ?v_7 ?v_20)))) (let ((?v_23 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_21)))) (?v_24 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_21)))) (?v_25 (c_sort type_alloc_table ?alloc)) (?v_54 (c_sort ?v_0 ?w9)) (?v_26 (c_sort ?v_0 ?w8)) (?v_27 (c_sort ?v_0 ?w7)) (?v_32 (c_sort ?v_0 ?w6)) (?v_37 (c_sort ?v_0 ?w5)) (?v_40 (c_sort ?v_0 ?w4)) (?v_43 (c_sort ?v_0 ?w2))) (let ((?v_30 (base_addr ?v_26)) (?v_28 (base_addr ?v_27)) (?v_29 (c_sort ?v_0 (acc ?v_7 ?v_26)))) (let ((?v_34 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_29)))) (?v_35 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_29)))) (?v_31 (c_sort ?v_0 (acc ?v_7 ?v_27)))) (let ((?v_59 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_31)))) (?v_60 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_31)))) (?v_33 (base_addr ?v_32)) (?v_36 (c_sort ?v_0 (acc ?v_7 ?v_32)))) (let ((?v_46 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_36)))) (?v_47 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_36)))) (?v_38 (base_addr ?v_37)) (?v_39 (c_sort ?v_0 (acc ?v_7 ?v_37)))) (let ((?v_48 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_39)))) (?v_49 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_39)))) (?v_41 (base_addr ?v_40)) (?v_42 (c_sort ?v_0 (acc ?v_7 ?v_40)))) (let ((?v_50 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_42)))) (?v_51 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_42)))) (?v_44 (base_addr ?v_43)) (?v_45 (c_sort ?v_0 (acc ?v_7 ?v_43)))) (let ((?v_52 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_45)))) (?v_53 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_45)))) (?v_66 (valid ?v_25 ?v_14)) (?v_61 (c_sort ?v_0 ?w10)) (?v_56 (base_addr ?v_54)) (?v_55 (c_sort ?v_0 (acc ?v_7 ?v_54)))) (let ((?v_57 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_55)))) (?v_58 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_55)))) (?v_63 (base_addr ?v_61)) (?v_62 (c_sort ?v_0 (acc ?v_7 ?v_61)))) (let ((?v_64 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_62)))) (?v_65 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_62))))) (=> (and (and (not (= ?v_5 ?v_1)) (and (and (not (= ?v_1 ?v_12)) (not (= ?v_1 ?v_13))) (and (not (= ?v_5 ?v_16)) (not (= ?v_5 ?v_17))))) (and (and (not (= ?v_5 ?v_11)) (and (and (not (= ?v_11 ?v_12)) (not (= ?v_11 ?v_13))) (and (not (= ?v_5 ?v_18)) (not (= ?v_5 ?v_19))))) (and (and (not (= ?v_1 ?v_11)) (and (and (not (= ?v_11 ?v_16)) (not (= ?v_11 ?v_17))) (and (not (= ?v_1 ?v_18)) (not (= ?v_1 ?v_19))))) (and (and (not (= ?v_22 ?v_1)) (and (and (not (= ?v_1 ?v_23)) (not (= ?v_1 ?v_24))) (and (not (= ?v_22 ?v_16)) (not (= ?v_22 ?v_17))))) (and (and (not (= ?v_22 ?v_11)) (and (and (not (= ?v_11 ?v_23)) (not (= ?v_11 ?v_24))) (and (not (= ?v_22 ?v_18)) (not (= ?v_22 ?v_19))))) (and (valid ?v_25 ?v_54) (and (valid ?v_25 ?v_26) (and (valid ?v_25 ?v_27) (and (valid ?v_25 ?v_32) (and (valid ?v_25 ?v_37) (and (valid ?v_25 ?v_40) (and (valid ?v_25 ?v_3) (and (valid ?v_25 ?v_43) (and (valid ?v_25 ?v_20) (and (and (not (= ?v_30 ?v_28)) (and (and (not (= ?v_28 ?v_34)) (not (= ?v_28 ?v_35))) (and (not (= ?v_30 ?v_59)) (not (= ?v_30 ?v_60))))) (and (and (not (= ?v_30 ?v_33)) (and (and (not (= ?v_33 ?v_34)) (not (= ?v_33 ?v_35))) (and (not (= ?v_30 ?v_46)) (not (= ?v_30 ?v_47))))) (and (and (not (= ?v_30 ?v_38)) (and (and (not (= ?v_38 ?v_34)) (not (= ?v_38 ?v_35))) (and (not (= ?v_30 ?v_48)) (not (= ?v_30 ?v_49))))) (and (and (not (= ?v_30 ?v_41)) (and (and (not (= ?v_41 ?v_34)) (not (= ?v_41 ?v_35))) (and (not (= ?v_30 ?v_50)) (not (= ?v_30 ?v_51))))) (and (and (not (= ?v_30 ?v_5)) (and (and (not (= ?v_5 ?v_34)) (not (= ?v_5 ?v_35))) (and (not (= ?v_30 ?v_12)) (not (= ?v_30 ?v_13))))) (and (and (not (= ?v_30 ?v_44)) (and (and (not (= ?v_44 ?v_34)) (not (= ?v_44 ?v_35))) (and (not (= ?v_30 ?v_52)) (not (= ?v_30 ?v_53))))) (and (and (not (= ?v_30 ?v_22)) (and (and (not (= ?v_22 ?v_34)) (not (= ?v_22 ?v_35))) (and (not (= ?v_30 ?v_23)) (not (= ?v_30 ?v_24))))) (and (valid ?v_25 ?v_8) (and ?v_66 (and (and (not (= ?v_33 ?v_38)) (and (and (not (= ?v_38 ?v_46)) (not (= ?v_38 ?v_47))) (and (not (= ?v_33 ?v_48)) (not (= ?v_33 ?v_49))))) (and (and (not (= ?v_33 ?v_41)) (and (and (not (= ?v_41 ?v_46)) (not (= ?v_41 ?v_47))) (and (not (= ?v_33 ?v_50)) (not (= ?v_33 ?v_51))))) (and (and (not (= ?v_33 ?v_5)) (and (and (not (= ?v_5 ?v_46)) (not (= ?v_5 ?v_47))) (and (not (= ?v_33 ?v_12)) (not (= ?v_33 ?v_13))))) (and (and (not (= ?v_33 ?v_44)) (and (and (not (= ?v_44 ?v_46)) (not (= ?v_44 ?v_47))) (and (not (= ?v_33 ?v_52)) (not (= ?v_33 ?v_53))))) (and (and (not (= ?v_33 ?v_22)) (and (and (not (= ?v_22 ?v_46)) (not (= ?v_22 ?v_47))) (and (not (= ?v_33 ?v_23)) (not (= ?v_33 ?v_24))))) (and (and (not (= ?v_30 ?v_1)) (and (and (not (= ?v_1 ?v_34)) (not (= ?v_1 ?v_35))) (and (not (= ?v_30 ?v_16)) (not (= ?v_30 ?v_17))))) (and (and (not (= ?v_30 ?v_11)) (and (and (not (= ?v_11 ?v_34)) (not (= ?v_11 ?v_35))) (and (not (= ?v_30 ?v_18)) (not (= ?v_30 ?v_19))))) (and (and (not (= ?v_41 ?v_5)) (and (and (not (= ?v_5 ?v_50)) (not (= ?v_5 ?v_51))) (and (not (= ?v_41 ?v_12)) (not (= ?v_41 ?v_13))))) (and (and (not (= ?v_41 ?v_44)) (and (and (not (= ?v_44 ?v_50)) (not (= ?v_44 ?v_51))) (and (not (= ?v_41 ?v_52)) (not (= ?v_41 ?v_53))))) (and (and (not (= ?v_41 ?v_22)) (and (and (not (= ?v_22 ?v_50)) (not (= ?v_22 ?v_51))) (and (not (= ?v_41 ?v_23)) (not (= ?v_41 ?v_24))))) (and (and (not (= ?v_33 ?v_1)) (and (and (not (= ?v_1 ?v_46)) (not (= ?v_1 ?v_47))) (and (not (= ?v_33 ?v_16)) (not (= ?v_33 ?v_17))))) (and (and (not (= ?v_33 ?v_11)) (and (and (not (= ?v_11 ?v_46)) (not (= ?v_11 ?v_47))) (and (not (= ?v_33 ?v_18)) (not (= ?v_33 ?v_19))))) (and (and (not (= ?v_44 ?v_22)) (and (and (not (= ?v_22 ?v_52)) (not (= ?v_22 ?v_53))) (and (not (= ?v_44 ?v_23)) (not (= ?v_44 ?v_24))))) (and (and (not (= ?v_41 ?v_1)) (and (and (not (= ?v_1 ?v_50)) (not (= ?v_1 ?v_51))) (and (not (= ?v_41 ?v_16)) (not (= ?v_41 ?v_17))))) (and (and (not (= ?v_41 ?v_11)) (and (and (not (= ?v_11 ?v_50)) (not (= ?v_11 ?v_51))) (and (not (= ?v_41 ?v_18)) (not (= ?v_41 ?v_19))))) (and (valid ?v_25 ?v_61) (and (and (not (= ?v_44 ?v_1)) (and (and (not (= ?v_1 ?v_52)) (not (= ?v_1 ?v_53))) (and (not (= ?v_44 ?v_16)) (not (= ?v_44 ?v_17))))) (and (and (not (= ?v_44 ?v_11)) (and (and (not (= ?v_11 ?v_52)) (not (= ?v_11 ?v_53))) (and (not (= ?v_44 ?v_18)) (not (= ?v_44 ?v_19))))) (and (and (not (= ?v_56 ?v_30)) (and (and (not (= ?v_30 ?v_57)) (not (= ?v_30 ?v_58))) (and (not (= ?v_56 ?v_34)) (not (= ?v_56 ?v_35))))) (and (and (not (= ?v_56 ?v_28)) (and (and (not (= ?v_28 ?v_57)) (not (= ?v_28 ?v_58))) (and (not (= ?v_56 ?v_59)) (not (= ?v_56 ?v_60))))) (and (and (not (= ?v_56 ?v_33)) (and (and (not (= ?v_33 ?v_57)) (not (= ?v_33 ?v_58))) (and (not (= ?v_56 ?v_46)) (not (= ?v_56 ?v_47))))) (and (and (not (= ?v_56 ?v_38)) (and (and (not (= ?v_38 ?v_57)) (not (= ?v_38 ?v_58))) (and (not (= ?v_56 ?v_48)) (not (= ?v_56 ?v_49))))) (and (and (not (= ?v_63 ?v_56)) (and (and (not (= ?v_56 ?v_64)) (not (= ?v_56 ?v_65))) (and (not (= ?v_63 ?v_57)) (not (= ?v_63 ?v_58))))) (and (and (not (= ?v_56 ?v_41)) (and (and (not (= ?v_41 ?v_57)) (not (= ?v_41 ?v_58))) (and (not (= ?v_56 ?v_50)) (not (= ?v_56 ?v_51))))) (and (and (not (= ?v_63 ?v_30)) (and (and (not (= ?v_30 ?v_64)) (not (= ?v_30 ?v_65))) (and (not (= ?v_63 ?v_34)) (not (= ?v_63 ?v_35))))) (and (and (not (= ?v_56 ?v_5)) (and (and (not (= ?v_5 ?v_57)) (not (= ?v_5 ?v_58))) (and (not (= ?v_56 ?v_12)) (not (= ?v_56 ?v_13))))) (and (and (not (= ?v_63 ?v_28)) (and (and (not (= ?v_28 ?v_64)) (not (= ?v_28 ?v_65))) (and (not (= ?v_63 ?v_59)) (not (= ?v_63 ?v_60))))) (and (and (not (= ?v_56 ?v_44)) (and (and (not (= ?v_44 ?v_57)) (not (= ?v_44 ?v_58))) (and (not (= ?v_56 ?v_52)) (not (= ?v_56 ?v_53))))) (and (and (not (= ?v_63 ?v_33)) (and (and (not (= ?v_33 ?v_64)) (not (= ?v_33 ?v_65))) (and (not (= ?v_63 ?v_46)) (not (= ?v_63 ?v_47))))) (and (and (not (= ?v_56 ?v_22)) (and (and (not (= ?v_22 ?v_57)) (not (= ?v_22 ?v_58))) (and (not (= ?v_56 ?v_23)) (not (= ?v_56 ?v_24))))) (and (and (not (= ?v_63 ?v_38)) (and (and (not (= ?v_38 ?v_64)) (not (= ?v_38 ?v_65))) (and (not (= ?v_63 ?v_48)) (not (= ?v_63 ?v_49))))) (and (and (not (= ?v_63 ?v_41)) (and (and (not (= ?v_41 ?v_64)) (not (= ?v_41 ?v_65))) (and (not (= ?v_63 ?v_50)) (not (= ?v_63 ?v_51))))) (and (and (not (= ?v_63 ?v_5)) (and (and (not (= ?v_5 ?v_64)) (not (= ?v_5 ?v_65))) (and (not (= ?v_63 ?v_12)) (not (= ?v_63 ?v_13))))) (and (and (not (= ?v_63 ?v_44)) (and (and (not (= ?v_44 ?v_64)) (not (= ?v_44 ?v_65))) (and (not (= ?v_63 ?v_52)) (not (= ?v_63 ?v_53))))) (and (and (not (= ?v_63 ?v_22)) (and (and (not (= ?v_22 ?v_64)) (not (= ?v_22 ?v_65))) (and (not (= ?v_63 ?v_23)) (not (= ?v_63 ?v_24))))) (and (and (not (= ?v_28 ?v_33)) (and (and (not (= ?v_33 ?v_59)) (not (= ?v_33 ?v_60))) (and (not (= ?v_28 ?v_46)) (not (= ?v_28 ?v_47))))) (and (and (not (= ?v_28 ?v_38)) (and (and (not (= ?v_38 ?v_59)) (not (= ?v_38 ?v_60))) (and (not (= ?v_28 ?v_48)) (not (= ?v_28 ?v_49))))) (and (and (not (= ?v_28 ?v_41)) (and (and (not (= ?v_41 ?v_59)) (not (= ?v_41 ?v_60))) (and (not (= ?v_28 ?v_50)) (not (= ?v_28 ?v_51))))) (and (and (not (= ?v_28 ?v_5)) (and (and (not (= ?v_5 ?v_59)) (not (= ?v_5 ?v_60))) (and (not (= ?v_28 ?v_12)) (not (= ?v_28 ?v_13))))) (and (and (not (= ?v_28 ?v_44)) (and (and (not (= ?v_44 ?v_59)) (not (= ?v_44 ?v_60))) (and (not (= ?v_28 ?v_52)) (not (= ?v_28 ?v_53))))) (and (and (not (= ?v_28 ?v_22)) (and (and (not (= ?v_22 ?v_59)) (not (= ?v_22 ?v_60))) (and (not (= ?v_28 ?v_23)) (not (= ?v_28 ?v_24))))) (and (and (not (= ?v_56 ?v_1)) (and (and (not (= ?v_1 ?v_57)) (not (= ?v_1 ?v_58))) (and (not (= ?v_56 ?v_16)) (not (= ?v_56 ?v_17))))) (and (and (not (= ?v_56 ?v_11)) (and (and (not (= ?v_11 ?v_57)) (not (= ?v_11 ?v_58))) (and (not (= ?v_56 ?v_18)) (not (= ?v_56 ?v_19))))) (and (and (not (= ?v_63 ?v_1)) (and (and (not (= ?v_1 ?v_64)) (not (= ?v_1 ?v_65))) (and (not (= ?v_63 ?v_16)) (not (= ?v_63 ?v_17))))) (and (and (not (= ?v_63 ?v_11)) (and (and (not (= ?v_11 ?v_64)) (not (= ?v_11 ?v_65))) (and (not (= ?v_63 ?v_18)) (not (= ?v_63 ?v_19))))) (and (and (not (= ?v_38 ?v_41)) (and (and (not (= ?v_41 ?v_48)) (not (= ?v_41 ?v_49))) (and (not (= ?v_38 ?v_50)) (not (= ?v_38 ?v_51))))) (and (and (not (= ?v_38 ?v_5)) (and (and (not (= ?v_5 ?v_48)) (not (= ?v_5 ?v_49))) (and (not (= ?v_38 ?v_12)) (not (= ?v_38 ?v_13))))) (and (and (not (= ?v_38 ?v_44)) (and (and (not (= ?v_44 ?v_48)) (not (= ?v_44 ?v_49))) (and (not (= ?v_38 ?v_52)) (not (= ?v_38 ?v_53))))) (and (and (not (= ?v_38 ?v_22)) (and (and (not (= ?v_22 ?v_48)) (not (= ?v_22 ?v_49))) (and (not (= ?v_38 ?v_23)) (not (= ?v_38 ?v_24))))) (and (and (not (= ?v_28 ?v_1)) (and (and (not (= ?v_1 ?v_59)) (not (= ?v_1 ?v_60))) (and (not (= ?v_28 ?v_16)) (not (= ?v_28 ?v_17))))) (and (and (not (= ?v_28 ?v_11)) (and (and (not (= ?v_11 ?v_59)) (not (= ?v_11 ?v_60))) (and (not (= ?v_28 ?v_18)) (not (= ?v_28 ?v_19))))) (and (and (not (= ?v_5 ?v_44)) (and (and (not (= ?v_44 ?v_12)) (not (= ?v_44 ?v_13))) (and (not (= ?v_5 ?v_52)) (not (= ?v_5 ?v_53))))) (and (and (not (= ?v_5 ?v_22)) (and (and (not (= ?v_22 ?v_12)) (not (= ?v_22 ?v_13))) (and (not (= ?v_5 ?v_23)) (not (= ?v_5 ?v_24))))) (and (and (not (= ?v_38 ?v_1)) (and (and (not (= ?v_1 ?v_48)) (not (= ?v_1 ?v_49))) (and (not (= ?v_38 ?v_16)) (not (= ?v_38 ?v_17))))) (and (and (not (= ?v_38 ?v_11)) (and (and (not (= ?v_11 ?v_48)) (not (= ?v_11 ?v_49))) (and (not (= ?v_38 ?v_18)) (not (= ?v_38 ?v_19))))) (and (separation1 ?v_6 ?v_9) (and (valid_acc ?v_9) (and (valid_acc ?v_6) (and (valid_acc_range ?v_9 5) (valid_acc_range ?v_6 5))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (=> ?v_66 (forall ((?anonymous_2_v1_global0 c_unique)) (forall ((?anonymous_2_v2_global0 c_unique)) (forall ((?intM_global0 c_unique)) (let ((?v_67 (type_memory c_int type_global)) (?v_69 (type_pset type_global))) (let ((?v_68 (c_sort ?v_69 (pset_singleton ?v_14))) (?v_70 (offset ?v_8))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global) (c_sort ?v_67 ?anonymous_2_v1_global0) ?v_68) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global) (c_sort ?v_67 ?anonymous_2_v2_global0) ?v_68)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global) (c_sort ?v_67 ?intM_global0) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_14)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_14)))) 0 4)))))) (and (<= 0 ?v_70) (< ?v_70 (block_length ?v_25 ?v_8)))))))))))))))))))))))))))))))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibe99bbe.smt2-229-(check-sat)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-86-(declare-fun type_pointer (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:87:(declare-fun type_addr (c_type) c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-88-(declare-fun type_alloc_table () c_type)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-89-(declare-fun block_length (c_ssorted c_ssorted) Int)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:90:(declare-fun base_addr (c_ssorted) c_unique)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-91-(declare-fun offset (c_ssorted) Int)
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-110-(assert (forall ((?t_12_122_70 c_type)) (forall ((?p_121_71 c_unique)) (forall ((?i_120_72 Int)) (forall ((?j_119_73 Int)) (let ((?v_0 (type_pointer ?t_12_122_70))) (let ((?v_1 (c_sort ?v_0 ?p_121_71))) (= (shift (c_sort ?v_0 (shift ?v_1 ?i_120_72)) ?j_119_73) (shift ?v_1 (+ ?i_120_72 ?j_119_73))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:111:(assert (forall ((?t_13_125_74 c_type)) (forall ((?p_124_75 c_unique)) (forall ((?i_123_76 Int)) (let ((?v_0 (type_pointer ?t_13_125_74))) (let ((?v_1 (c_sort ?v_0 ?p_124_75))) (= (base_addr (c_sort ?v_0 (shift ?v_1 ?i_123_76))) (base_addr ?v_1))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-112-(assert (forall ((?t_14_129_77 c_type)) (forall ((?a_128_78 c_unique)) (forall ((?p_127_79 c_unique)) (forall ((?i_126_80 Int)) (let ((?v_1 (c_sort type_alloc_table ?a_128_78)) (?v_0 (type_pointer ?t_14_129_77))) (let ((?v_2 (c_sort ?v_0 ?p_127_79))) (= (block_length ?v_1 (c_sort ?v_0 (shift ?v_2 ?i_126_80))) (block_length ?v_1 ?v_2)))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-154-(assert (forall ((?t_42_259_176 c_type)) (forall ((?t_41_258_177 c_type)) (forall ((?l_257_178 c_unique)) (forall ((?m_256_179 c_unique)) (forall ((?p_255_180 c_unique)) (let ((?v_0 (type_pointer ?t_42_259_176))) (=> (not_in_pset (c_sort ?v_0 ?p_255_180) (c_sort (type_pset ?t_42_259_176) (pset_star (c_sort (type_pset ?t_41_258_177) ?l_257_178) (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179)))) (forall ((?p1_254_181 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_41_258_177) ?p1_254_181))) (=> (= ?p_255_180 (acc (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_41_258_177) ?l_257_178)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:155:(assert (forall ((?t_43_263_182 c_type)) (forall ((?p_262_183 c_unique)) (forall ((?l_261_184 c_unique)) (let ((?v_0 (type_pset ?t_43_263_182))) (=> (forall ((?p1_260_185 c_unique)) (let ((?v_1 (type_pointer ?t_43_263_182))) (let ((?v_2 (c_sort ?v_1 ?p1_260_185))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_261_184))) (not (= (base_addr (c_sort ?v_1 ?p_262_183)) (base_addr ?v_2))))))) (not_in_pset (c_sort (type_pointer ?t_43_263_182) ?p_262_183) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_261_184))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:156:(assert (forall ((?t_44_267_186 c_type)) (forall ((?p_266_187 c_unique)) (forall ((?l_265_188 c_unique)) (let ((?v_0 (type_pset ?t_44_267_186))) (=> (not_in_pset (c_sort (type_pointer ?t_44_267_186) ?p_266_187) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_265_188)))) (forall ((?p1_264_189 c_unique)) (let ((?v_1 (type_pointer ?t_44_267_186))) (let ((?v_2 (c_sort ?v_1 ?p1_264_189))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_265_188))) (not (= (base_addr (c_sort ?v_1 ?p_266_187)) (base_addr ?v_2)))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-157-(assert (forall ((?t_45_274_190 c_type)) (forall ((?p_273_191 c_unique)) (forall ((?l_272_192 c_unique)) (forall ((?a_271_193 Int)) (forall ((?b_270_194 Int)) (let ((?v_0 (type_pset ?t_45_274_190))) (=> (forall ((?p1_269_195 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) (c_sort ?v_0 ?l_272_192)) (forall ((?i_268_196 Int)) (=> (and (<= ?a_271_193 ?i_268_196) (<= ?i_268_196 ?b_270_194)) (not (= ?p_273_191 (shift (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) ?i_268_196))))))) (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p_273_191) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_272_192) ?a_271_193 ?b_270_194)))))))))))
##############################################
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-178-(declare-fun separation1 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:179:(assert (forall ((?t_78_404_321 c_type)) (forall ((?t_77_403_322 c_type)) (forall ((?m1_402_323 c_unique)) (forall ((?m2_401_324 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_77_403_322) ?t_78_404_321))) (= (separation1 (c_sort ?v_0 ?m1_402_323) (c_sort ?v_0 ?m2_401_324)) (forall ((?p_400_325 c_unique)) (forall ((?a_399_326 c_unique)) (let ((?v_1 (type_pointer ?t_77_403_322)) (?v_2 (c_sort (type_pointer ?t_78_404_321) ?p_400_325))) (=> (valid (c_sort type_alloc_table ?a_399_326) ?v_2) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_402_323) ?v_2))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_401_324) ?v_2))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-180-(declare-fun separation1_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:181:(assert (forall ((?t_80_412_327 c_type)) (forall ((?t_79_411_328 c_type)) (forall ((?m1_410_329 c_unique)) (forall ((?m2_409_330 c_unique)) (forall ((?size_408_331 Int)) (let ((?v_0 (type_memory (type_pointer ?t_79_411_328) ?t_80_412_327))) (= (separation1_range1 (c_sort ?v_0 ?m1_410_329) (c_sort ?v_0 ?m2_409_330) ?size_408_331) (forall ((?p_407_332 c_unique)) (forall ((?a_406_333 c_unique)) (=> (valid (c_sort type_alloc_table ?a_406_333) (c_sort (type_pointer ?t_80_412_327) ?p_407_332)) (forall ((?i_405_334 Int)) (let ((?v_1 (type_pointer ?t_79_411_328)) (?v_2 (type_pointer ?t_80_412_327))) (let ((?v_3 (c_sort ?v_2 ?p_407_332))) (=> (and (<= 0 ?i_405_334) (< ?i_405_334 ?size_408_331)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_410_329) (c_sort ?v_2 (shift ?v_3 ?i_405_334))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_409_330) ?v_3))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-182-(declare-fun separation1_range (c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:183:(assert (forall ((?t_82_420_335 c_type)) (forall ((?t_81_419_336 c_type)) (forall ((?m_418_337 c_unique)) (forall ((?size_417_338 Int)) (= (separation1_range (c_sort (type_memory (type_pointer ?t_81_419_336) ?t_82_420_335) ?m_418_337) ?size_417_338) (forall ((?p_416_339 c_unique)) (forall ((?a_415_340 c_unique)) (=> (valid (c_sort type_alloc_table ?a_415_340) (c_sort (type_pointer ?t_82_420_335) ?p_416_339)) (forall ((?i1_414_341 Int)) (forall ((?i2_413_342 Int)) (let ((?v_0 (type_pointer ?t_81_419_336))) (let ((?v_2 (c_sort (type_memory ?v_0 ?t_82_420_335) ?m_418_337)) (?v_1 (type_pointer ?t_82_420_335))) (let ((?v_3 (c_sort ?v_1 ?p_416_339))) (=> (and (<= 0 ?i1_414_341) (< ?i1_414_341 ?size_417_338)) (=> (and (<= 0 ?i2_413_342) (< ?i2_413_342 ?size_417_338)) (=> (not (= ?i1_414_341 ?i2_413_342)) (not (= (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i1_414_341))))) (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i2_413_342))))))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-184-(declare-fun separation2 (c_ssorted c_ssorted) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:185:(assert (forall ((?t_84_426_343 c_type)) (forall ((?t_83_425_344 c_type)) (forall ((?m1_424_345 c_unique)) (forall ((?m2_423_346 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_83_425_344) ?t_84_426_343))) (= (separation2 (c_sort ?v_0 ?m1_424_345) (c_sort ?v_0 ?m2_423_346)) (forall ((?p1_422_347 c_unique)) (forall ((?p2_421_348 c_unique)) (let ((?v_1 (type_pointer ?t_83_425_344)) (?v_2 (type_pointer ?t_84_426_343))) (=> (not (= ?p1_422_347 ?p2_421_348)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_424_345) (c_sort ?v_2 ?p1_422_347)))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_423_346) (c_sort ?v_2 ?p2_421_348)))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-186-(declare-fun separation2_range1 (c_ssorted c_ssorted Int) Bool)
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2:187:(assert (forall ((?t_86_435_349 c_type)) (forall ((?t_85_434_350 c_type)) (forall ((?m1_433_351 c_unique)) (forall ((?m2_432_352 c_unique)) (forall ((?size_431_353 Int)) (let ((?v_0 (type_memory (type_pointer ?t_85_434_350) ?t_86_435_349))) (= (separation2_range1 (c_sort ?v_0 ?m1_433_351) (c_sort ?v_0 ?m2_432_352) ?size_431_353) (forall ((?p_430_354 c_unique)) (forall ((?q_429_355 c_unique)) (forall ((?a_428_356 c_unique)) (forall ((?i_427_357 Int)) (let ((?v_1 (type_pointer ?t_85_434_350)) (?v_2 (type_pointer ?t_86_435_349))) (=> (and (<= 0 ?i_427_357) (< ?i_427_357 ?size_431_353)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_433_351) (c_sort ?v_2 (shift (c_sort ?v_2 ?p_430_354) ?i_427_357))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_432_352) (c_sort ?v_2 ?q_429_355))))))))))))))))))))
cvc4-1.8/test/regress/regress1/quantifiers/smtlibf957ea.smt2-188-(declare-fun on_heap (c_ssorted c_ssorted) Bool)
##############################################
cvc4-1.8/test/regress/regress2/ooo.rf6.smt2-13-(declare-fun BOOOB_46_init_rob_head () Int)
cvc4-1.8/test/regress/regress2/ooo.rf6.smt2:14:(declare-fun Baddr () Int)
cvc4-1.8/test/regress/regress2/ooo.rf6.smt2-15-(declare-fun BOOOB_46_init_null_opcode () Int)
##############################################
cvc4-1.8/test/regress/regress3/pp-regfile.smtv1.smt2-123-(declare-fun NO_VALUE37 () Int)
cvc4-1.8/test/regress/regress3/pp-regfile.smtv1.smt2:124:(declare-fun ARB_ADDR () Int)
cvc4-1.8/test/regress/regress3/pp-regfile.smtv1.smt2-125-(declare-fun NO_VALUE3 () Int)
##############################################
cvc4-1.8/test/system/sep_log_api.cpp-224-    /* Find both sides of the PTO operator */
cvc4-1.8/test/system/sep_log_api.cpp:225:    Rational addr(
cvc4-1.8/test/system/sep_log_api.cpp-226-        smt.getValue(child.getChildren().at(0)).getConst<CVC4::Rational>());
##############################################
cvc4-1.8/test/unit/util/stats_black.h-69-    BackedStat<bool> backedBool("backedBool", true);
cvc4-1.8/test/unit/util/stats_black.h:70:    BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
cvc4-1.8/test/unit/util/stats_black.h-71-    HistogramStat<int64_t> histStat("hist");
##############################################
cvc4-1.8/debian/patches/03-remove-build-path.patch-11- 
cvc4-1.8/debian/patches/03-remove-build-path.patch:12: filename=`basename "$1" | sed 's,_template,,'`
cvc4-1.8/debian/patches/03-remove-build-path.patch-13-+template_rel="<CVC4>/"$(realpath --relative-to $CMAKE_SOURCE_DIR $1)
##############################################
cvc4-1.8/debian/patches/03-remove-build-path.patch-117- 
cvc4-1.8/debian/patches/03-remove-build-path.patch:118: filename=`basename "$1" | sed 's,_template,,'`
cvc4-1.8/debian/patches/03-remove-build-path.patch-119-+template_rel="<CVC4>/"$(realpath --relative-to $CMAKE_SOURCE_DIR $1)
##############################################
cvc4-1.8/debian/patches/03-remove-build-path.patch-265- "
cvc4-1.8/debian/patches/03-remove-build-path.patch:266:   cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'`
cvc4-1.8/debian/patches/03-remove-build-path.patch-267-   metakind_constDeleters="${metakind_constDeleters}
##############################################
cvc4-1.8/.pc/02-install-lib-dir.patch/CMakeLists.txt-182-# Determine number of threads available, used to configure (default) parallel
cvc4-1.8/.pc/02-install-lib-dir.patch/CMakeLists.txt:183:# execution of custom test targets (can be overriden with ARGS=-jN).
cvc4-1.8/.pc/02-install-lib-dir.patch/CMakeLists.txt-184-
##############################################
cvc4-1.8/.pc/02-install-lib-dir.patch/CMakeLists.txt-218-message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
cvc4-1.8/.pc/02-install-lib-dir.patch/CMakeLists.txt:219:include(Config${CMAKE_BUILD_TYPE})
cvc4-1.8/.pc/02-install-lib-dir.patch/CMakeLists.txt-220-
##############################################
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkexpr-19-
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkexpr:20:filename=`basename "$1" | sed 's,_template,,'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkexpr-21-
##############################################
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkexpr-309-done
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkexpr:310:error=`expr "$text" : '.*\${\([^}]*\)}.*'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkexpr-311-if [ -n "$error" ]; then
##############################################
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkkind-18-
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkkind:19:filename=`basename "$1" | sed 's,_template,,'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkkind-20-
##############################################
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkkind-415-done
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkkind:416:error=`expr "$text" : '.*\${\([^}]*\)}.*'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkkind-417-if [ -n "$error" ]; then
##############################################
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-281-"
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind:282:  cname=`echo "$2" | awk 'BEGIN {FS="::"} {print$NF}'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-283-  metakind_constDeleters="${metakind_constDeleters}
##############################################
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-320-  elif expr "$nc" : '[0-9][0-9]*:$' >/dev/null; then
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind:321:    let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-322-    ub="expr::NodeValue::MAX_CHILDREN"
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-323-  elif expr "$nc" : '[0-9][0-9]*:[0-9][0-9]*$' >/dev/null; then
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind:324:    let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-325-    if [ $ub -lt $lb ]; then
##############################################
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-343-function primitive_type {
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind:344:  strip=`expr "$1" : ' *\(.*\)\* *'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-345-  if [ -n "$strip" ]; then
##############################################
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-420-done
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind:421:error=`expr "$text" : '.*\${\([^}]*\)}.*'`
cvc4-1.8/.pc/03-remove-build-path.patch/src/expr/mkmetakind-422-if [ -n "$error" ]; then
##############################################
cvc4-1.8/CMakeLists.txt-182-# Determine number of threads available, used to configure (default) parallel
cvc4-1.8/CMakeLists.txt:183:# execution of custom test targets (can be overriden with ARGS=-jN).
cvc4-1.8/CMakeLists.txt-184-
##############################################
cvc4-1.8/CMakeLists.txt-218-message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
cvc4-1.8/CMakeLists.txt:219:include(Config${CMAKE_BUILD_TYPE})
cvc4-1.8/CMakeLists.txt-220-