fix Inconsistent Results from consequences Interface Based on Constan…

…t Names (see: Z3Prover#6916)
ptr1120 · Sep 24, 2023 · 638c5d9 · 638c5d9
1 parent da43edf
commit 638c5d9
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
@@ -10,7 +10,7 @@ variables:
   msanEnv: 'CC=clang LDFLAGS="-L../libcxx/libcxx_msan/lib -lc++abi -Wl,-rpath=../libcxx/libcxx_msan/lib" CXX=clang++ CXXFLAGS="${CXXFLAGS} -stdlib=libc++ -fsanitize-memory-track-origins -fsanitize=memory -fPIE -fno-omit-frame-pointer -g -O2" CFLAGS="${CFLAGS} -stdlib=libc -fsanitize=memory -fsanitize-memory-track-origins -fno-omit-frame-pointer -g -O2"'
   ReleaseVersion: '4.11.2'
   NugetVersion: '$(ReleaseVersion)-ast-size-cancel-token-0003'
-  NugetDescription: 'Build on Azure: BuildId $(Build.BuildId) * native change: starting size of ast hash table, see also https://github.com/Z3Prover/z3/pull/5040 *  Dotnet: removed IDecRefQueue and dispose via cancellation token'
+  NugetDescription: 'Build on Azure: BuildId $(Build.BuildId) * native change: starting size of ast hash table, see also https://github.com/Z3Prover/z3/pull/5040 *  Dotnet: removed IDecRefQueue and dispose via cancellation token * fix Inconsistent Results from consequences Interface Based on Constant Names (see: https://github.com/Z3Prover/z3/issues/6916)'
 
 stages:
 

diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
@@ -243,7 +243,7 @@ namespace smt {
                     lit.neg();
 
                 literal lit = mk_diseq(k, v);
-                literals.push_back(lit);
+                literals.push_back(~lit);
                 mk_clause(literals.size(), literals.data(), nullptr);
                 TRACE("context", display_literals_verbose(tout, literals.size(), literals.data()););
             }