fix: handling pointers in bitwuzla builder

Author: metametamoon

lib/Solver/BitwuzlaBuilder.cpp

@@ -1113,6 +1113,11 @@ Term BitwuzlaBuilder::constructActual(ref<Expr> e, int *width_out) {
     assert(*width_out != 1 && "uncanonicalized FNeg");
     return ctx->mk_term(Kind::FP_NEG, {arg});
   }
+  case Expr::Pointer:
+  case Expr::ConstantPointer: {
+    PointerExpr *pointerExpr = cast<PointerExpr>(e);
+    return constructActual(pointerExpr->getValue(), width_out);
+  };
 
 // unused due to canonicalization
 #if 0
@@ -1124,7 +1129,7 @@ case Expr::Sge:
 #endif
 
   default:
-    assert(0 && "unhandled Expr type");
+    klee_error("unhandled Expr type");
     return getTrue();
   }
 }

test/Bidirectional/Memory/cond-function-pointer-change.c

@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward --use-concretizing-solver=false %t.bc 2> %t.log
 // RUN: FileCheck %s -input-file=%t.log
 
 #include "klee/klee.h"

test/Bidirectional/Memory/cond-stack-pointer-change.c

@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm %O0opt -c -fno-discard-value-names -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward %t.bc 2> %t.log
+// RUN: %klee --write-kqueries --output-dir=%t.klee-out --max-propagations=5 --max-stack-frames=15 --execution-mode=bidirectional --tmp-skip-fns-in-init=false --initialize-in-join-blocks --function-call-reproduce=reach_error --skip-not-lazy-initialized --forward-ticks=0 --backward-ticks=5 --skip-not-symbolic-objects --write-xml-tests --debug-log=rootpob,backward,conflict,closepob,reached,init --debug-constraints=backward --use-concretizing-solver=false %t.bc 2> %t.log
 // RUN: FileCheck %s -input-file=%t.log
 
 #include "klee/klee.h"